diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 98fada2b5c6..717639a083a 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -92,7 +92,7 @@ You can create a new `Array` with a new value for a key in O(log(N)) time, or effectively constant. ```k - syntax Array ::= Array "[" key: Int "<-" value: KItem "]" [function, klabel(_[_<-_]), symbol] + syntax Array ::= Array "[" key: Int "<-" value: KItem "]" [function, symbol(_[_<-_])] ``` ### Array reset @@ -237,7 +237,7 @@ other words, one unbound variable is linear, two is quadratic, three is cubic, etc. ```k - syntax Map ::= Map Map [left, function, hook(MAP.concat), klabel(_Map_), symbol, assoc, comm, unit(.Map), element(_|->_), index(0), format(%1%n%2)] + syntax Map ::= Map Map [left, function, hook(MAP.concat), symbol(_Map_), assoc, comm, unit(.Map), element(_|->_), index(0), format(%1%n%2)] ``` ### Map unit @@ -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] + syntax Map ::= ".Map" [function, total, hook(MAP.unit), symbol(.Map)] ``` ### 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, injective] + syntax Map ::= KItem "|->" KItem [function, total, hook(MAP.element), symbol(_|->_), injective] syntax priority _|->_ > _Map_ .Map syntax non-assoc _|->_ @@ -268,7 +268,7 @@ time is effectively constant. The value is `#False` if the key is not in the map (in particular, this will yield an exception during concrete execution). ```k - syntax KItem ::= Map "[" KItem "]" [function, hook(MAP.lookup), klabel(Map:lookup), symbol] + syntax KItem ::= Map "[" KItem "]" [function, hook(MAP.lookup), symbol(Map:lookup)] ``` ### Map lookup with default @@ -278,7 +278,7 @@ total function that assigns a specific default value if the key is not present in the map. This operation is also O(log(N)), or effectively constant. ```k - syntax KItem ::= Map "[" KItem "]" "orDefault" KItem [function, total, hook(MAP.lookupOrDefault), klabel(Map:lookupOrDefault)] + syntax KItem ::= Map "[" KItem "]" "orDefault" KItem [function, total, hook(MAP.lookupOrDefault), symbol(Map:lookupOrDefault)] ``` ### Map update @@ -287,7 +287,7 @@ You can insert a key/value pair into a map in O(log(N)) time, or effectively constant. ```k - syntax Map ::= Map "[" key: KItem "<-" value: KItem "]" [function, total, klabel(Map:update), symbol, hook(MAP.update), prefer] + syntax Map ::= Map "[" key: KItem "<-" value: KItem "]" [function, total, symbol(Map:update), hook(MAP.update), prefer] ``` ### Map delete @@ -296,7 +296,7 @@ You can remove a key/value pair from a map via its key in O(log(N)) time, or effectively constant. ```k - syntax Map ::= Map "[" KItem "<-" "undef" "]" [function, total, hook(MAP.remove), klabel(_[_<-undef]), symbol] + syntax Map ::= Map "[" KItem "<-" "undef" "]" [function, total, hook(MAP.remove), symbol(_[_<-undef])] ``` ### Map difference @@ -370,7 +370,7 @@ You can get a `List` of all the values in a map in O(N) time. You can get the number of key/value pairs in a map in O(1) time. ```k - syntax Int ::= size(Map) [function, total, hook(MAP.size), klabel(sizeMap)] + syntax Int ::= size(Map) [function, total, hook(MAP.size), symbol(sizeMap)] ``` ### Map inclusion @@ -390,7 +390,7 @@ will always be returned for the same map, but no guarantee is given that two different maps will return the same element, even if they are similar. ```k - syntax KItem ::= choice(Map) [function, hook(MAP.choice), klabel(Map:choice)] + syntax KItem ::= choice(Map) [function, hook(MAP.choice), symbol(Map:choice)] ``` ### Implementation of Maps @@ -488,7 +488,7 @@ module RANGEMAP ### Range, bounded inclusively below and exclusively above. ```k - syntax Range ::= "[" KItem "," KItem ")" [klabel(RangeMap:Range), symbol] + syntax Range ::= "[" KItem "," KItem ")" [symbol(RangeMap:Range)] syntax RangeMap [hook(RANGEMAP.RangeMap)] ``` @@ -505,7 +505,7 @@ thrown during concrete execution. This operation is O(N*log(M)) (where N is the size of the smaller map and M is the size of the larger map). ```k - syntax RangeMap ::= RangeMap RangeMap [left, function, hook(RANGEMAP.concat), klabel(_RangeMap_), symbol, assoc, comm, unit(.RangeMap), element(_r|->_), index(0), format(%1%n%2)] + syntax RangeMap ::= RangeMap RangeMap [left, function, hook(RANGEMAP.concat), symbol(_RangeMap_), assoc, comm, unit(.RangeMap), element(_r|->_), index(0), format(%1%n%2)] ``` ### Range map unit @@ -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] + syntax RangeMap ::= ".RangeMap" [function, total, hook(RANGEMAP.unit), symbol(.RangeMap)] ``` ### 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, injective] + syntax RangeMap ::= Range "r|->" KItem [function, hook(RANGEMAP.elementRng), symbol(_r|->_), injective] syntax priority _r|->_ > _RangeMap_ .RangeMap syntax non-assoc _r|->_ @@ -535,7 +535,7 @@ time (where N is the size of the `RangeMap`). This will yield an exception during concrete execution if the key is not in the range map. ```k - syntax KItem ::= RangeMap "[" KItem "]" [function, hook(RANGEMAP.lookup), klabel(RangeMap:lookup), symbol] + syntax KItem ::= RangeMap "[" KItem "]" [function, hook(RANGEMAP.lookup), symbol(RangeMap:lookup)] ``` ### Range map lookup with default @@ -546,7 +546,7 @@ in the `RangeMap`. This operation is also O(log(N)) (where N is the size of the range map). ```k - syntax KItem ::= RangeMap "[" KItem "]" "orDefault" KItem [function, total, hook(RANGEMAP.lookupOrDefault), klabel(RangeMap:lookupOrDefault)] + syntax KItem ::= RangeMap "[" KItem "]" "orDefault" KItem [function, total, hook(RANGEMAP.lookupOrDefault), symbol(RangeMap:lookupOrDefault)] ``` ### Range map lookup for range of key @@ -556,7 +556,7 @@ O(log(N)) time (where N is the size of the `RangeMap`). This will yield an exception during concrete execution if the key is not in the range map. ```k - syntax Range ::= "find_range" "(" RangeMap "," KItem ")" [function, hook(RANGEMAP.find_range), klabel(RangeMap:find_range)] + syntax Range ::= "find_range" "(" RangeMap "," KItem ")" [function, hook(RANGEMAP.find_range), symbol(RangeMap:find_range)] ``` ### Range map update @@ -566,7 +566,7 @@ is the size of the `RangeMap`). Any ranges adjacent to or overlapping with the range to be inserted will be updated accordingly. ```k - syntax RangeMap ::= RangeMap "[" keyRange: Range "<-" value: KItem "]" [function, klabel(RangeMap:update), symbol, hook(RANGEMAP.updateRng), prefer] + syntax RangeMap ::= RangeMap "[" keyRange: Range "<-" value: KItem "]" [function, symbol(RangeMap:update), hook(RANGEMAP.updateRng), prefer] ``` ### Range map delete @@ -576,7 +576,7 @@ is the size of the `RangeMap`). If all or any part of the range is present in the range map, it will be removed. ```k - syntax RangeMap ::= RangeMap "[" Range "<-" "undef" "]" [function, hook(RANGEMAP.removeRng), klabel(_r[_<-undef]), symbol] + syntax RangeMap ::= RangeMap "[" Range "<-" "undef" "]" [function, hook(RANGEMAP.removeRng), symbol(_r[_<-undef])] ``` ### Range map difference @@ -657,7 +657,7 @@ size of the `RangeMap`). You can get the number of range/value pairs in a `RangeMap` in O(1) time. ```k - syntax Int ::= size(RangeMap) [function, total, hook(RANGEMAP.size), klabel(sizeRangeMap)] + syntax Int ::= size(RangeMap) [function, total, hook(RANGEMAP.size), symbol(sizeRangeMap)] ``` ### Range map inclusion @@ -679,7 +679,7 @@ that two different range maps will return the same element, even if they are similar. ```k - syntax KItem ::= choice(RangeMap) [function, hook(RANGEMAP.choice), klabel(RangeMap:choice)] + syntax KItem ::= choice(RangeMap) [function, hook(RANGEMAP.choice), symbol(RangeMap:choice)] endmodule ``` @@ -718,7 +718,7 @@ number of unbound keys being mached. In other words, one unbound variable is linear, two is quadratic, three is cubic, etc. ```k - syntax Set ::= Set Set [left, function, hook(SET.concat), klabel(_Set_), symbol, assoc, comm, unit(.Set), idem, element(SetItem), format(%1%n%2)] + syntax Set ::= Set Set [left, function, hook(SET.concat), symbol(_Set_), assoc, comm, unit(.Set), idem, element(SetItem), format(%1%n%2)] ``` ### Set unit @@ -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] + syntax Set ::= ".Set" [function, total, hook(SET.unit), symbol(.Set)] ``` ### Set elements @@ -734,7 +734,7 @@ The set with zero elements is represented by `.Set`. An element of a `Set` is constructed via the `SetItem` operator. ```k - syntax Set ::= SetItem(KItem) [function, total, hook(SET.element), klabel(SetItem), symbol, injective] + syntax Set ::= SetItem(KItem) [function, total, hook(SET.element), symbol(SetItem), injective] ``` ### Set union @@ -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), klabel(Set:difference), symbol] + syntax Set ::= Set "-Set" Set [function, total, hook(SET.difference), symbol(Set:difference)] ``` ### Set membership @@ -774,7 +774,7 @@ elements in the first set that are not present in the second set. You can compute whether an element is a member of a set in O(1) time. ```k - syntax Bool ::= KItem "in" Set [function, total, hook(SET.in), klabel(Set:in), symbol] + syntax Bool ::= KItem "in" Set [function, total, hook(SET.in), symbol(Set:in)] ``` ### Set inclusion @@ -801,7 +801,7 @@ element will always be returned for the same set, but no guarantee is given that two different sets will return the same element, even if they are similar. ```k - syntax KItem ::= choice(Set) [function, hook(SET.choice), klabel(Set:choice)] + syntax KItem ::= choice(Set) [function, hook(SET.choice), symbol(Set:choice)] ``` ```k @@ -926,7 +926,7 @@ side, it is O(N), where N is the number of elements matched on the front and back of the list. ```k - syntax List ::= List List [left, function, total, hook(LIST.concat), klabel(_List_), symbol, smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), format(%1%n%2)] + syntax List ::= List List [left, function, total, hook(LIST.concat), symbol(_List_), smtlib(smt_seq_concat), assoc, unit(.List), element(ListItem), format(%1%n%2)] ``` ### List unit @@ -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)] + syntax List ::= ".List" [function, total, hook(LIST.unit), symbol(.List), smtlib(smt_seq_nil)] ``` ### List elements @@ -942,7 +942,7 @@ The list with zero elements is represented by `.List`. An element of a `List` is constucted via the `ListItem` operator. ```k - syntax List ::= ListItem(KItem) [function, total, hook(LIST.element), klabel(ListItem), symbol, smtlib(smt_seq_elem)] + syntax List ::= ListItem(KItem) [function, total, hook(LIST.element), symbol(ListItem), smtlib(smt_seq_elem)] ``` ### List prepend @@ -950,7 +950,7 @@ An element of a `List` is constucted via the `ListItem` operator. An element can be added to the front of a `List` using the `pushList` operator. ```k - syntax List ::= pushList(KItem, List) [function, total, hook(LIST.push), klabel(pushList), symbol] + syntax List ::= pushList(KItem, List) [function, total, hook(LIST.push), symbol(pushList)] rule pushList(K::KItem, L1::List) => ListItem(K) L1 ``` @@ -962,7 +962,7 @@ list, and negative indices are -1-indexed from the end of the list. In other words, 0 is the first element and -1 is the last element. ```k - syntax KItem ::= List "[" Int "]" [function, hook(LIST.get), klabel(List:get), symbol] + syntax KItem ::= List "[" Int "]" [function, hook(LIST.get), symbol(List:get)] ``` ### List update @@ -971,7 +971,7 @@ You can create a new `List` with a new value at a particular index in O(log(N)) time, or effectively constant. ```k - syntax List ::= List "[" index: Int "<-" value: KItem "]" [function, hook(LIST.update), klabel(List:set)] + syntax List ::= List "[" index: Int "<-" value: KItem "]" [function, hook(LIST.update), symbol(List:set)] ``` ### List of identical elements @@ -1009,7 +1009,7 @@ of the list and `fromBack` elements from the back of the list in O((fromFront+fromBack)*log(N)) time, or effectively linear. ```k - syntax List ::= range(List, fromFront: Int, fromBack: Int) [function, hook(LIST.range), klabel(List:range), symbol] + syntax List ::= range(List, fromFront: Int, fromBack: Int) [function, hook(LIST.range), symbol(List:range)] ``` ### List membership @@ -1018,7 +1018,7 @@ You can compute whether an element is in a list in O(N) time. For repeated comparisons, it is much better to first convert to a set using `List2Set`. ```k - syntax Bool ::= KItem "in" List [function, total, hook(LIST.in), klabel(_inList_)] + syntax Bool ::= KItem "in" List [function, total, hook(LIST.in), symbol(_inList_)] ``` ### List size @@ -1026,7 +1026,7 @@ comparisons, it is much better to first convert to a set using `List2Set`. You can get the number of elements of a list in O(1) time. ```k - syntax Int ::= size(List) [function, total, hook(LIST.size), klabel (sizeList), smtlib(smt_seq_len)] + syntax Int ::= size(List) [function, total, hook(LIST.size), symbol(sizeList), smtlib(smt_seq_len)] ``` ```k @@ -1106,16 +1106,16 @@ 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), 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), 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)] + syntax Bool ::= "notBool" Bool [function, total, symbol(notBool_), smt-hook(not), group(boolOperation), hook(BOOL.not)] + > Bool "andBool" Bool [function, total, symbol(_andBool_), left, smt-hook(and), group(boolOperation), hook(BOOL.and)] + | Bool "andThenBool" Bool [function, total, symbol(_andThenBool_), left, smt-hook(and), group(boolOperation), hook(BOOL.andThen)] + | Bool "xorBool" Bool [function, total, symbol(_xorBool_), left, smt-hook(xor), group(boolOperation), hook(BOOL.xor)] + | Bool "orBool" Bool [function, total, symbol(_orBool_), left, smt-hook(or), group(boolOperation), hook(BOOL.or)] + | Bool "orElseBool" Bool [function, total, symbol(_orElseBool_), left, smt-hook(or), group(boolOperation), hook(BOOL.orElse)] + | Bool "impliesBool" Bool [function, total, symbol(_impliesBool_), left, smt-hook(=>), group(boolOperation), hook(BOOL.implies)] > left: - Bool "==Bool" Bool [function, total, klabel(_==Bool_), symbol, left, comm, smt-hook(=), hook(BOOL.eq)] - | Bool "=/=Bool" Bool [function, total, klabel(_=/=Bool_), symbol, left, comm, smt-hook(distinct), hook(BOOL.ne)] + Bool "==Bool" Bool [function, total, symbol(_==Bool_), left, comm, smt-hook(=), hook(BOOL.eq)] + | Bool "=/=Bool" Bool [function, total, symbol(_=/=Bool_), left, comm, smt-hook(distinct), hook(BOOL.ne)] ``` ### Implementation of Booleans @@ -1234,31 +1234,31 @@ You can: * Compute the bitwise inclusive-or of two integers in twos-complement. ```k - syntax Int ::= "~Int" Int [function, klabel(~Int_), symbol, total, hook(INT.not), smtlib(notInt)] + syntax Int ::= "~Int" Int [function, symbol(~Int_), total, hook(INT.not), smtlib(notInt)] > left: - 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)] + Int "^Int" Int [function, symbol(_^Int_), left, smt-hook(^), hook(INT.pow)] + | Int "^%Int" Int Int [function, symbol(_^%Int__), left, smt-hook((mod (^ #1 #2) #3)), hook(INT.powmod)] > left: - Int "*Int" Int [function, total, klabel(_*Int_), symbol, left, comm, smt-hook(*), hook(INT.mul)] + Int "*Int" Int [function, total, symbol(_*Int_), 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), hook(INT.tdiv)] - | Int "%Int" Int [function, klabel(_%Int_), symbol, left, smt-hook(mod), hook(INT.tmod)] + | Int "/Int" Int [function, symbol(_/Int_), left, smt-hook(div), hook(INT.tdiv)] + | Int "%Int" Int [function, symbol(_%Int_), 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)] + | Int "divInt" Int [function, symbol(_divInt_), left, smt-hook(div), hook(INT.ediv)] + | Int "modInt" Int [function, symbol(_modInt_), left, smt-hook(mod), hook(INT.emod)] > left: - 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)] + Int "+Int" Int [function, total, symbol(_+Int_), left, comm, smt-hook(+), hook(INT.add)] + | Int "-Int" Int [function, total, symbol(_-Int_), left, smt-hook(-), hook(INT.sub)] > left: - Int ">>Int" Int [function, klabel(_>>Int_), symbol, left, hook(INT.shr), smtlib(shrInt)] - | Int "<>Int" Int [function, symbol(_>>Int_), left, hook(INT.shr), smtlib(shrInt)] + | Int "< left: - Int "&Int" Int [function, total, klabel(_&Int_), symbol, left, comm, hook(INT.and), smtlib(andInt)] + Int "&Int" Int [function, total, symbol(_&Int_), left, comm, hook(INT.and), smtlib(andInt)] > left: - Int "xorInt" Int [function, total, klabel(_xorInt_), symbol, left, comm, hook(INT.xor), smtlib(xorInt)] + Int "xorInt" Int [function, total, symbol(_xorInt_), left, comm, hook(INT.xor), smtlib(xorInt)] > left: - Int "|Int" Int [function, total, klabel(_|Int_), symbol, left, comm, hook(INT.or), smtlib(orInt)] + Int "|Int" Int [function, total, symbol(_|Int_), left, comm, hook(INT.or), smtlib(orInt)] ``` ### Integer minimum and maximum @@ -1310,12 +1310,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(<=), 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)] + syntax Bool ::= Int "<=Int" Int [function, total, symbol(_<=Int_), smt-hook(<=), hook(INT.le)] + | Int "=Int" Int [function, total, symbol(_>=Int_), smt-hook(>=), hook(INT.ge)] + | Int ">Int" Int [function, total, symbol(_>Int_), smt-hook(>), hook(INT.gt)] + | Int "==Int" Int [function, total, symbol(_==Int_), comm, smt-hook(=), hook(INT.eq)] + | Int "=/=Int" Int [function, total, symbol(_=/=Int_), comm, smt-hook(distinct), hook(INT.ne)] ``` ### Divides @@ -1627,7 +1627,7 @@ IEEE 754 arithmetic. `0.0 ==Float -0.0` is also true. | 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(fp.eq), hook(FLOAT.eq), symbol(_==Float_)] | Float "=/=Float" Float [function, comm, smt-hook((not (fp.eq #1 #2)))] rule F1:Float =/=Float F2:Float => notBool (F1 ==Float F2) @@ -1796,7 +1796,7 @@ implement floating-point numbers. ```k syntax String ::= Float2String ( Float ) [function, total, hook(STRING.float2string)] - syntax String ::= Float2String ( Float , format: String ) [function, klabel(FloatFormat), hook(STRING.floatFormat)] + syntax String ::= Float2String ( Float , format: String ) [function, symbol(FloatFormat), hook(STRING.floatFormat)] syntax Float ::= String2Float ( String ) [function, hook(STRING.string2float)] ``` @@ -2024,8 +2024,8 @@ endian (ie, least significant byte first) or big endian (ie, most significant byte first). ```k - syntax Endianness ::= "LE" [klabel(littleEndianBytes), symbol] - | "BE" [klabel(bigEndianBytes), symbol] + syntax Endianness ::= "LE" [symbol(littleEndianBytes)] + | "BE" [symbol(bigEndianBytes)] ``` ### Signedness @@ -2034,8 +2034,8 @@ When converting to/from an integer, byte arrays can be treated as either signed or unsigned. ```k - syntax Signedness ::= "Signed" [klabel(signedBytes), symbol] - | "Unsigned" [klabel(unsignedBytes), symbol] + syntax Signedness ::= "Signed" [symbol(signedBytes)] + | "Unsigned" [symbol(unsignedBytes)] ``` ### Integer and Bytes conversion @@ -2065,7 +2065,7 @@ to the nearest byte. ```k syntax Int ::= Bytes2Int(Bytes, Endianness, Signedness) [function, total, hook(BYTES.bytes2int)] syntax Bytes ::= Int2Bytes(length: Int, Int, Endianness) [function, total, hook(BYTES.int2bytes)] - | Int2Bytes(Int, Endianness, Signedness) [function, total, klabel(Int2BytesNoLen)] + | Int2Bytes(Int, Endianness, Signedness) [function, total, symbol(Int2BytesNoLen)] ``` ### String and Bytes conversion @@ -2283,8 +2283,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, group(equalEqualK)] - | K "=/=K" K [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, group(notEqualEqualK)] + K "==K" K [function, total, comm, smt-hook(=), hook(KEQUAL.eq), symbol(_==K_), group(equalEqualK)] + | K "=/=K" K [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), symbol(_=/=K_), group(notEqualEqualK)] syntax priority equalEqualK notEqualEqualK > boolOperation mlOp @@ -2341,7 +2341,7 @@ module K-REFLECTION syntax K ::= "#configuration" [function, impure, hook(KREFLECTION.configuration)] syntax String ::= #sort(K) [function, hook(KREFLECTION.sort)] syntax KItem ::= #fresh(String) [function, hook(KREFLECTION.fresh), impure] - syntax KItem ::= getKLabel(K) [function, hook(KREFLECTION.getKLabel)] + syntax KItem ::= getsymbol(K) [function, hook(KREFLECTION.getKLabel)] syntax K ::= #getenv(String) [function, impure, hook(KREFLECTION.getenv)] @@ -2352,7 +2352,7 @@ module K-REFLECTION syntax List ::= #argv() [function, hook(KREFLECTION.argv)] syntax {Sort} String ::= #unparseKORE(Sort) [function, hook(KREFLECTION.printKORE)] - syntax IOError ::= "#noParse" "(" String ")" [klabel(#noParse), symbol] + syntax IOError ::= "#noParse" "(" String ")" [symbol(#noParse)] endmodule ``` @@ -2389,76 +2389,76 @@ a library function. If the `errno` returned is not one of the below errnos known to K, `#unknownIOError` is returned along with the integer errno value. ```k - syntax IOError ::= "#EOF" [klabel(#EOF), symbol] - | #unknownIOError(errno: Int) [klabel(#unknownIOError), symbol] - | "#E2BIG" [klabel(#E2BIG), symbol] - | "#EACCES" [klabel(#EACCES), symbol] - | "#EAGAIN" [klabel(#EAGAIN), symbol] - | "#EBADF" [klabel(#EBADF), symbol] - | "#EBUSY" [klabel(#EBUSY), symbol] - | "#ECHILD" [klabel(#ECHILD), symbol] - | "#EDEADLK" [klabel(#EDEADLK), symbol] - | "#EDOM" [klabel(#EDOM), symbol] - | "#EEXIST" [klabel(#EEXIST), symbol] - | "#EFAULT" [klabel(#EFAULT), symbol] - | "#EFBIG" [klabel(#EFBIG), symbol] - | "#EINTR" [klabel(#EINTR), symbol] - | "#EINVAL" [klabel(#EINVAL), symbol] - | "#EIO" [klabel(#EIO), symbol] - | "#EISDIR" [klabel(#EISDIR), symbol] - | "#EMFILE" [klabel(#EMFILE), symbol] - | "#EMLINK" [klabel(#EMLINK), symbol] - | "#ENAMETOOLONG" [klabel(#ENAMETOOLONG), symbol] - | "#ENFILE" [klabel(#ENFILE), symbol] - | "#ENODEV" [klabel(#ENODEV), symbol] - | "#ENOENT" [klabel(#ENOENT), symbol] - | "#ENOEXEC" [klabel(#ENOEXEC), symbol] - | "#ENOLCK" [klabel(#ENOLCK), symbol] - | "#ENOMEM" [klabel(#ENOMEM), symbol] - | "#ENOSPC" [klabel(#ENOSPC), symbol] - | "#ENOSYS" [klabel(#ENOSYS), symbol] - | "#ENOTDIR" [klabel(#ENOTDIR), symbol] - | "#ENOTEMPTY" [klabel(#ENOTEMPTY), symbol] - | "#ENOTTY" [klabel(#ENOTTY), symbol] - | "#ENXIO" [klabel(#ENXIO), symbol] - | "#EPERM" [klabel(#EPERM), symbol] - | "#EPIPE" [klabel(#EPIPE), symbol] - | "#ERANGE" [klabel(#ERANGE), symbol] - | "#EROFS" [klabel(#EROFS), symbol] - | "#ESPIPE" [klabel(#ESPIPE), symbol] - | "#ESRCH" [klabel(#ESRCH), symbol] - | "#EXDEV" [klabel(#EXDEV), symbol] - | "#EWOULDBLOCK" [klabel(#EWOULDBLOCK), symbol] - | "#EINPROGRESS" [klabel(#EINPROGRESS), symbol] - | "#EALREADY" [klabel(#EALREADY), symbol] - | "#ENOTSOCK" [klabel(#ENOTSOCK), symbol] - | "#EDESTADDRREQ" [klabel(#EDESTADDRREQ), symbol] - | "#EMSGSIZE" [klabel(#EMSGSIZE), symbol] - | "#EPROTOTYPE" [klabel(#EPROTOTYPE), symbol] - | "#ENOPROTOOPT" [klabel(#ENOPROTOOPT), symbol] - | "#EPROTONOSUPPORT" [klabel(#EPROTONOSUPPORT), symbol] - | "#ESOCKTNOSUPPORT" [klabel(#ESOCKTNOSUPPORT), symbol] - | "#EOPNOTSUPP" [klabel(#EOPNOTSUPP), symbol] - | "#EPFNOSUPPORT" [klabel(#EPFNOSUPPORT), symbol] - | "#EAFNOSUPPORT" [klabel(#EAFNOSUPPORT), symbol] - | "#EADDRINUSE" [klabel(#EADDRINUSE), symbol] - | "#EADDRNOTAVAIL" [klabel(#EADDRNOTAVAIL), symbol] - | "#ENETDOWN" [klabel(#ENETDOWN), symbol] - | "#ENETUNREACH" [klabel(#ENETUNREACH), symbol] - | "#ENETRESET" [klabel(#ENETRESET), symbol] - | "#ECONNABORTED" [klabel(#ECONNABORTED), symbol] - | "#ECONNRESET" [klabel(#ECONNRESET), symbol] - | "#ENOBUFS" [klabel(#ENOBUFS), symbol] - | "#EISCONN" [klabel(#EISCONN), symbol] - | "#ENOTCONN" [klabel(#ENOTCONN), symbol] - | "#ESHUTDOWN" [klabel(#ESHUTDOWN), symbol] - | "#ETOOMANYREFS" [klabel(#ETOOMANYREFS), symbol] - | "#ETIMEDOUT" [klabel(#ETIMEDOUT), symbol] - | "#ECONNREFUSED" [klabel(#ECONNREFUSED), symbol] - | "#EHOSTDOWN" [klabel(#EHOSTDOWN), symbol] - | "#EHOSTUNREACH" [klabel(#EHOSTUNREACH), symbol] - | "#ELOOP" [klabel(#ELOOP), symbol] - | "#EOVERFLOW" [klabel(#EOVERFLOW), symbol] + syntax IOError ::= "#EOF" [symbol(#EOF)] + | #unknownIOError(errno: Int) [symbol(#unknownIOError)] + | "#E2BIG" [symbol(#E2BIG)] + | "#EACCES" [symbol(#EACCES)] + | "#EAGAIN" [symbol(#EAGAIN)] + | "#EBADF" [symbol(#EBADF)] + | "#EBUSY" [symbol(#EBUSY)] + | "#ECHILD" [symbol(#ECHILD)] + | "#EDEADLK" [symbol(#EDEADLK)] + | "#EDOM" [symbol(#EDOM)] + | "#EEXIST" [symbol(#EEXIST)] + | "#EFAULT" [symbol(#EFAULT)] + | "#EFBIG" [symbol(#EFBIG)] + | "#EINTR" [symbol(#EINTR)] + | "#EINVAL" [symbol(#EINVAL)] + | "#EIO" [symbol(#EIO)] + | "#EISDIR" [symbol(#EISDIR)] + | "#EMFILE" [symbol(#EMFILE)] + | "#EMLINK" [symbol(#EMLINK)] + | "#ENAMETOOLONG" [symbol(#ENAMETOOLONG)] + | "#ENFILE" [symbol(#ENFILE)] + | "#ENODEV" [symbol(#ENODEV)] + | "#ENOENT" [symbol(#ENOENT)] + | "#ENOEXEC" [symbol(#ENOEXEC)] + | "#ENOLCK" [symbol(#ENOLCK)] + | "#ENOMEM" [symbol(#ENOMEM)] + | "#ENOSPC" [symbol(#ENOSPC)] + | "#ENOSYS" [symbol(#ENOSYS)] + | "#ENOTDIR" [symbol(#ENOTDIR)] + | "#ENOTEMPTY" [symbol(#ENOTEMPTY)] + | "#ENOTTY" [symbol(#ENOTTY)] + | "#ENXIO" [symbol(#ENXIO)] + | "#EPERM" [symbol(#EPERM)] + | "#EPIPE" [symbol(#EPIPE)] + | "#ERANGE" [symbol(#ERANGE)] + | "#EROFS" [symbol(#EROFS)] + | "#ESPIPE" [symbol(#ESPIPE)] + | "#ESRCH" [symbol(#ESRCH)] + | "#EXDEV" [symbol(#EXDEV)] + | "#EWOULDBLOCK" [symbol(#EWOULDBLOCK)] + | "#EINPROGRESS" [symbol(#EINPROGRESS)] + | "#EALREADY" [symbol(#EALREADY)] + | "#ENOTSOCK" [symbol(#ENOTSOCK)] + | "#EDESTADDRREQ" [symbol(#EDESTADDRREQ)] + | "#EMSGSIZE" [symbol(#EMSGSIZE)] + | "#EPROTOTYPE" [symbol(#EPROTOTYPE)] + | "#ENOPROTOOPT" [symbol(#ENOPROTOOPT)] + | "#EPROTONOSUPPORT" [symbol(#EPROTONOSUPPORT)] + | "#ESOCKTNOSUPPORT" [symbol(#ESOCKTNOSUPPORT)] + | "#EOPNOTSUPP" [symbol(#EOPNOTSUPP)] + | "#EPFNOSUPPORT" [symbol(#EPFNOSUPPORT)] + | "#EAFNOSUPPORT" [symbol(#EAFNOSUPPORT)] + | "#EADDRINUSE" [symbol(#EADDRINUSE)] + | "#EADDRNOTAVAIL" [symbol(#EADDRNOTAVAIL)] + | "#ENETDOWN" [symbol(#ENETDOWN)] + | "#ENETUNREACH" [symbol(#ENETUNREACH)] + | "#ENETRESET" [symbol(#ENETRESET)] + | "#ECONNABORTED" [symbol(#ECONNABORTED)] + | "#ECONNRESET" [symbol(#ECONNRESET)] + | "#ENOBUFS" [symbol(#ENOBUFS)] + | "#EISCONN" [symbol(#EISCONN)] + | "#ENOTCONN" [symbol(#ENOTCONN)] + | "#ESHUTDOWN" [symbol(#ESHUTDOWN)] + | "#ETOOMANYREFS" [symbol(#ETOOMANYREFS)] + | "#ETIMEDOUT" [symbol(#ETIMEDOUT)] + | "#ECONNREFUSED" [symbol(#ECONNREFUSED)] + | "#EHOSTDOWN" [symbol(#EHOSTDOWN)] + | "#EHOSTUNREACH" [symbol(#EHOSTUNREACH)] + | "#ELOOP" [symbol(#ELOOP)] + | "#EOVERFLOW" [symbol(#EOVERFLOW)] ``` ### I/O result sorts @@ -2594,7 +2594,7 @@ reason about in K should not be implemented via the `#system` operator. ```k syntax KItem ::= #system ( String ) [function, hook(IO.system), impure] - | "#systemResult" "(" Int /* exit code */ "," String /* stdout */ "," String /* stderr */ ")" [klabel(#systemResult), symbol] + | "#systemResult" "(" Int /* exit code */ "," String /* stdout */ "," String /* stderr */ ")" [symbol(#systemResult)] ``` ### Temporary files @@ -2606,7 +2606,7 @@ For more info on the argument to `#mkstemp`, see `man mkstemp`. ```k syntax IOFile ::= #mkstemp(template: String) [function, hook(IO.mkstemp), impure] syntax IOFile ::= IOError - | "#tempFile" "(" path: String "," fd: Int ")" [klabel(#tempFile), symbol] + | "#tempFile" "(" path: String "," fd: Int ")" [symbol(#tempFile)] ``` ### Deleting a file @@ -2627,7 +2627,7 @@ containing `name` in its name. The file is only flushed to disk when rewriting finishes. ```k - syntax K ::= #logToFile(name: String, value: String) [function, total, hook(IO.log), impure, returnsUnit, klabel(#logToFile), symbol] + syntax K ::= #logToFile(name: String, value: String) [function, total, hook(IO.log), impure, returnsUnit, symbol(#logToFile)] ``` Strings can also be logged via the logging mechanisms available to the backend. @@ -2636,7 +2636,7 @@ Haskell backend, a log message of type InfoUserLog is created with the specified text. ```k - syntax K ::= #log(value: String) [function, total, hook(IO.logString), impure, returnsUnit, klabel(#log), symbol] + syntax K ::= #log(value: String) [function, total, hook(IO.logString), impure, returnsUnit, symbol(#log)] ``` Terms can also be logged to standard error in _surface syntax_, rather than as @@ -2647,8 +2647,8 @@ logged, which requires re-parsing the underlying K definition. Subsequent calls do not incur this overhead again; the definition is cached. ```k - syntax K ::= #trace(value: KItem) [function, total, hook(IO.traceTerm), impure, returnsUnit, klabel(#trace), symbol] - | #traceK(value: K) [function, total, hook(IO.traceTerm), impure, returnsUnit, klabel(#traceK), symbol] + syntax K ::= #trace(value: KItem) [function, total, hook(IO.traceTerm), impure, returnsUnit, symbol(#trace)] + | #traceK(value: K) [function, total, hook(IO.traceTerm), impure, returnsUnit, symbol(#traceK)] ``` ### Implementation of high-level I/O streams in K diff --git a/k-distribution/include/kframework/builtin/ffi.md b/k-distribution/include/kframework/builtin/ffi.md index 3bba4fdd94e..19028faeb11 100644 --- a/k-distribution/include/kframework/builtin/ffi.md +++ b/k-distribution/include/kframework/builtin/ffi.md @@ -29,31 +29,31 @@ to the `#ffiCall` function. These types roughly correspond to the types declared in `ffi.h` by libffi. ```k - syntax FFIType ::= "#void" [klabel(#ffi_void), symbol] - | "#uint8" [klabel(#ffi_uint8), symbol] - | "#sint8" [klabel(#ffi_sint8), symbol] - | "#uint16" [klabel(#ffi_uint16), symbol] - | "#sint16" [klabel(#ffi_sint16), symbol] - | "#uint32" [klabel(#ffi_uint32), symbol] - | "#sint32" [klabel(#ffi_sint32), symbol] - | "#uint64" [klabel(#ffi_uint64), symbol] - | "#sint64" [klabel(#ffi_sint64), symbol] - | "#float" [klabel(#ffi_float), symbol] - | "#double" [klabel(#ffi_double), symbol] - | "#uchar" [klabel(#ffi_uchar), symbol] - | "#schar" [klabel(#ffi_schar), symbol] - | "#ushort" [klabel(#ffi_ushort), symbol] - | "#sshort" [klabel(#ffi_sshort), symbol] - | "#uint" [klabel(#ffi_uint), symbol] - | "#sint" [klabel(#ffi_sint), symbol] - | "#ulong" [klabel(#ffi_ulong), symbol] - | "#slong" [klabel(#ffi_slong), symbol] - | "#longdouble" [klabel(#ffi_longdouble), symbol] - | "#pointer" [klabel(#ffi_pointer), symbol] - | "#complexfloat" [klabel(#ffi_complexfloat), symbol] - | "#complexdouble" [klabel(#ffi_complexdouble), symbol] - | "#complexlongdouble" [klabel(#ffi_complexlongdouble), symbol] - | "#struct" "(" List ")" [klabel(#ffi_struct), symbol] + syntax FFIType ::= "#void" [symbol(#ffi_void)] + | "#uint8" [symbol(#ffi_uint8)] + | "#sint8" [symbol(#ffi_sint8)] + | "#uint16" [symbol(#ffi_uint16)] + | "#sint16" [symbol(#ffi_sint16)] + | "#uint32" [symbol(#ffi_uint32)] + | "#sint32" [symbol(#ffi_sint32)] + | "#uint64" [symbol(#ffi_uint64)] + | "#sint64" [symbol(#ffi_sint64)] + | "#float" [symbol(#ffi_float)] + | "#double" [symbol(#ffi_double)] + | "#uchar" [symbol(#ffi_uchar)] + | "#schar" [symbol(#ffi_schar)] + | "#ushort" [symbol(#ffi_ushort)] + | "#sshort" [symbol(#ffi_sshort)] + | "#uint" [symbol(#ffi_uint)] + | "#sint" [symbol(#ffi_sint)] + | "#ulong" [symbol(#ffi_ulong)] + | "#slong" [symbol(#ffi_slong)] + | "#longdouble" [symbol(#ffi_longdouble)] + | "#pointer" [symbol(#ffi_pointer)] + | "#complexfloat" [symbol(#ffi_complexfloat)] + | "#complexdouble" [symbol(#ffi_complexdouble)] + | "#complexlongdouble" [symbol(#ffi_complexlongdouble)] + | "#struct" "(" List ")" [symbol(#ffi_struct)] endmodule module FFI diff --git a/k-distribution/include/kframework/builtin/json.md b/k-distribution/include/kframework/builtin/json.md index c02f831b21a..71dbb89b52c 100644 --- a/k-distribution/include/kframework/builtin/json.md +++ b/k-distribution/include/kframework/builtin/json.md @@ -20,11 +20,11 @@ module JSON-SYNTAX syntax JSONs ::= List{JSON,","} [symbol(JSONs)] syntax JSONKey ::= String - syntax JSON ::= "null" [klabel(JSONnull) , symbol] + syntax JSON ::= "null" [symbol(JSONnull)] | String | Int | Float | Bool - | JSONKey ":" JSON [klabel(JSONEntry) , symbol] - | "{" JSONs "}" [klabel(JSONObject) , symbol] - | "[" JSONs "]" [klabel(JSONList) , symbol] + | JSONKey ":" JSON [symbol(JSONEntry)] + | "{" JSONs "}" [symbol(JSONObject)] + | "[" JSONs "]" [symbol(JSONList)] endmodule ``` diff --git a/k-distribution/include/kframework/builtin/kast.md b/k-distribution/include/kframework/builtin/kast.md index e15d02d4eaa..1cc50f2a0ae 100644 --- a/k-distribution/include/kframework/builtin/kast.md +++ b/k-distribution/include/kframework/builtin/kast.md @@ -76,9 +76,9 @@ module KAST imports KSTRING imports BUILTIN-ID-TOKENS - syntax KBott ::= "#token" "(" KString "," KString ")" [klabel(#KToken), symbol] - | "#klabel" "(" KLabel ")" [klabel(#WrappedKLabel), symbol] - | KLabel "(" KList ")" [klabel(#KApply), symbol] + syntax KBott ::= "#token" "(" KString "," KString ")" [symbol(#KToken)] + | "#klabel" "(" KLabel ")" [symbol(#WrappedKLabel)] + | KLabel "(" KList ")" [symbol(#KApply)] syntax KItem ::= KBott syntax KLabel ::= r"`(\\\\`|\\\\\\\\|[^`\\\\\\n\\r])+`" [token] @@ -86,8 +86,8 @@ module KAST | r"[#a-z][a-zA-Z0-9]*" [token, prec(1)] syntax KList ::= K - | ".KList" [klabel(#EmptyKList), symbol] - | KList "," KList [klabel(#KList), left, assoc, unit(#EmptyKList), symbol, prefer] + | ".KList" [symbol(#EmptyKList)] + | KList "," KList [symbol(#KList), left, assoc, unit(#EmptyKList), prefer] endmodule @@ -95,9 +95,9 @@ endmodule module KSEQ imports KAST imports K-TOP-SORT - syntax K ::= ".K" [klabel(#EmptyK), symbol] - | "." [klabel(#EmptyK), symbol, deprecated, unparseAvoid] - syntax K ::= K "~>" K [klabel(#KSequence), left, assoc, unit(#EmptyK), symbol] + syntax K ::= ".K" [symbol(#EmptyK)] + | "." [symbol(#EmptyK), deprecated, unparseAvoid] + syntax K ::= K "~>" K [symbol(#KSequence), left, assoc, unit(#EmptyK)] syntax left #KSequence syntax {Sort} Sort ::= "(" Sort ")" [bracket, group(defaultBracket), applyPriority(1)] endmodule @@ -135,28 +135,28 @@ The correspondance between K symbols and KORE symbols is as follows: module ML-SYNTAX [not-lr1] imports SORT-K - syntax {Sort} Sort ::= "#Top" [klabel(#Top), symbol, group(mlUnary)] - | "#Bottom" [klabel(#Bottom), symbol, group(mlUnary)] - | "#Not" "(" Sort ")" [klabel(#Not), symbol, mlOp, group(mlUnary, mlOp)] + syntax {Sort} Sort ::= "#Top" [symbol(#Top), group(mlUnary)] + | "#Bottom" [symbol(#Bottom), group(mlUnary)] + | "#Not" "(" Sort ")" [symbol(#Not), mlOp, group(mlUnary, mlOp)] - syntax {Sort1, Sort2} Sort2 ::= "#Ceil" "(" Sort1 ")" [klabel(#Ceil), symbol, mlOp, group(mlUnary, mlOp)] - | "#Floor" "(" Sort1 ")" [klabel(#Floor), symbol, mlOp, group(mlUnary, mlOp)] - | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, group(mlEquals, mlOp), comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)] + syntax {Sort1, Sort2} Sort2 ::= "#Ceil" "(" Sort1 ")" [symbol(#Ceil), mlOp, group(mlUnary, mlOp)] + | "#Floor" "(" Sort1 ")" [symbol(#Floor), mlOp, group(mlUnary, mlOp)] + | "{" Sort1 "#Equals" Sort1 "}" [symbol(#Equals), mlOp, group(mlEquals, mlOp), comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)] syntax priority mlUnary > mlEquals > mlAnd - syntax {Sort} Sort ::= Sort "#And" Sort [klabel(#And), symbol, assoc, left, comm, unit(#Top), mlOp, group(mlAnd, mlOp), format(%i%1%d%n%2%n%i%3%d)] - > Sort "#Or" Sort [klabel(#Or), symbol, assoc, left, comm, unit(#Bottom), mlOp, group(mlOp), format(%i%1%d%n%2%n%i%3%d)] - > Sort "#Implies" Sort [klabel(#Implies), symbol, mlOp, group(mlImplies, mlOp), format(%i%1%d%n%2%n%i%3%d)] + syntax {Sort} Sort ::= Sort "#And" Sort [symbol(#And), assoc, left, comm, unit(#Top), mlOp, group(mlAnd, mlOp), format(%i%1%d%n%2%n%i%3%d)] + > Sort "#Or" Sort [symbol(#Or), assoc, left, comm, unit(#Bottom), mlOp, group(mlOp), format(%i%1%d%n%2%n%i%3%d)] + > Sort "#Implies" Sort [symbol(#Implies), mlOp, group(mlImplies, mlOp), format(%i%1%d%n%2%n%i%3%d)] syntax priority mlImplies > mlQuantifier - syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [klabel(#Exists), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)] - | "#Forall" Sort1 "." Sort2 [klabel(#Forall), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)] + syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [symbol(#Exists), mlOp, mlBinder, group(mlQuantifier, mlOp)] + | "#Forall" Sort1 "." Sort2 [symbol(#Forall), mlOp, mlBinder, group(mlQuantifier, mlOp)] - syntax {Sort} Sort ::= "#AG" "(" Sort ")" [klabel(#AG), symbol, mlOp, group(mlOp)] - | "#wEF" "(" Sort ")" [klabel(weakExistsFinally), symbol, mlOp, group(mlOp)] - | "#wAF" "(" Sort ")" [klabel(weakAlwaysFinally), symbol, mlOp, group(mlOp)] + syntax {Sort} Sort ::= "#AG" "(" Sort ")" [symbol(#AG), mlOp, group(mlOp)] + | "#wEF" "(" Sort ")" [symbol(weakExistsFinally), mlOp, group(mlOp)] + | "#wAF" "(" Sort ")" [symbol(weakAlwaysFinally), mlOp, group(mlOp)] endmodule ``` @@ -236,13 +236,13 @@ module KCELLS imports KAST syntax Cell - syntax Bag ::= Bag Bag [left, assoc, klabel(#cells), symbol, unit(#cells)] - | ".Bag" [klabel(#cells), symbol] - | ".::Bag" [klabel(#cells), symbol] + syntax Bag ::= Bag Bag [left, assoc, symbol(#cells), unit(#cells)] + | ".Bag" [symbol(#cells)] + | ".::Bag" [symbol(#cells)] | Cell syntax Bag ::= "(" Bag ")" [bracket] syntax KItem ::= Bag - syntax #RuleBody ::= "[" "[" K "]" "]" Bag [klabel(#withConfig), symbol, avoid] + syntax #RuleBody ::= "[" "[" K "]" "]" Bag [symbol(#withConfig), avoid] syntax non-assoc #withConfig syntax Bag ::= KBott endmodule @@ -272,10 +272,10 @@ module RULE-CELLS // if this module is imported, the parser automatically // generates, for all productions that have the attribute 'cell' or 'maincell', // a production like below: - //syntax Cell ::= "" #OptionalDots K #OptionalDots "" [klabel()] + //syntax Cell ::= "" #OptionalDots K #OptionalDots "" [symbol()] - syntax #OptionalDots ::= "..." [klabel(#dots), symbol] - | "" [klabel(#noDots), symbol] + syntax #OptionalDots ::= "..." [symbol(#dots)] + | "" [symbol(#noDots)] syntax Int // this production will be added by the compiler to help handle bang variables, @@ -286,7 +286,7 @@ module RULE-CELLS // this production will "vanish" after parsing finishes and not be picked up // by the compiler, which is the behavior we want in this case since an actual // production will be generated by the compiler later on. - syntax GeneratedCounterCell ::= "" Int "" [cell, klabel(), symbol, internal] + syntax GeneratedCounterCell ::= "" Int "" [cell, symbol(), internal] endmodule ``` @@ -309,12 +309,12 @@ module CONFIG-CELLS | #LowerId [token] | #UpperId [token] - syntax Cell ::= "<" #CellName #CellProperties ">" K "" [klabel(#configCell), symbol] - syntax Cell ::= "<" #CellName "/>" [klabel(#externalCell), symbol] + syntax Cell ::= "<" #CellName #CellProperties ">" K "" [symbol(#configCell)] + syntax Cell ::= "<" #CellName "/>" [symbol(#externalCell)] - syntax #CellProperties ::= #CellProperty #CellProperties [klabel(#cellPropertyList), symbol] - | "" [klabel(#cellPropertyListTerminator), symbol] - syntax #CellProperty ::= #CellName "=" KString [klabel(#cellProperty), symbol] + syntax #CellProperties ::= #CellProperty #CellProperties [symbol(#cellPropertyList)] + | "" [symbol(#cellPropertyListTerminator)] + syntax #CellProperty ::= #CellName "=" KString [symbol(#cellProperty)] endmodule ``` @@ -342,10 +342,10 @@ module REQUIRES-ENSURES syntax #RuleBody ::= K - syntax #RuleContent ::= #RuleBody [klabel("#ruleNoConditions"), symbol] - | #RuleBody "requires" Bool [klabel("#ruleRequires"), symbol] - | #RuleBody "ensures" Bool [klabel("#ruleEnsures"), symbol] - | #RuleBody "requires" Bool "ensures" Bool [klabel("#ruleRequiresEnsures"), symbol] + syntax #RuleContent ::= #RuleBody [symbol("#ruleNoConditions")] + | #RuleBody "requires" Bool [symbol("#ruleRequires")] + | #RuleBody "ensures" Bool [symbol("#ruleEnsures")] + | #RuleBody "requires" Bool "ensures" Bool [symbol("#ruleRequiresEnsures")] endmodule ``` @@ -401,12 +401,12 @@ module PROGRAM-LISTS imports SORT-K // if this module is imported, the parser automatically // replaces the default productions for lists: - // Es ::= E "," Es [userList("*"), klabel('_,_)] - // | ".Es" [userList("*"), klabel('.Es)] + // Es ::= E "," Es [userList("*"), symbol('_,_)] + // | ".Es" [userList("*"), symbol('.Es)] // into a series of productions more suitable for programs: - // Es#Terminator ::= "" [klabel('.Es)] - // Ne#Es ::= E "," Ne#Es [klabel('_,_)] - // | E Es#Terminator [klabel('_,_)] + // Es#Terminator ::= "" [symbol('.Es)] + // Ne#Es ::= E "," Ne#Es [symbol('_,_)] + // | E Es#Terminator [symbol('_,_)] // Es ::= Ne#Es // | Es#Terminator // if the list is * endmodule @@ -442,7 +442,7 @@ documentation. ```k module KREWRITE - syntax {Sort} Sort ::= Sort "=>" Sort [klabel(#KRewrite), symbol] + syntax {Sort} Sort ::= Sort "=>" Sort [symbol(#KRewrite)] syntax non-assoc #KRewrite syntax priority #KRewrite > #withConfig endmodule @@ -458,13 +458,13 @@ module K imports AUTO-FOLLOW imports KREWRITE - syntax {Sort} Sort ::= Sort "#as" Sort [klabel(#KAs), symbol] + syntax {Sort} Sort ::= Sort "#as" Sort [symbol(#KAs)] // functions that preserve sorts and can therefore have inner rewrites - syntax {Sort} Sort ::= "#fun" "(" Sort ")" "(" Sort ")" [klabel(#fun2), symbol, prefer] + syntax {Sort} Sort ::= "#fun" "(" Sort ")" "(" Sort ")" [symbol(#fun2), prefer] // functions that do not preserve sort and therefore cannot have inner rewrites - syntax {Sort1, Sort2} Sort1 ::= "#fun" "(" Sort2 "=>" Sort1 ")" "(" Sort2 ")" [klabel(#fun3), symbol] + syntax {Sort1, Sort2} Sort1 ::= "#fun" "(" Sort2 "=>" Sort1 ")" "(" Sort2 ")" [symbol(#fun3)] - syntax {Sort1, Sort2} Sort1 ::= "#let" Sort2 "=" Sort2 "#in" Sort1 [klabel(#let), symbol] + syntax {Sort1, Sort2} Sort1 ::= "#let" Sort2 "=" Sort2 "#in" Sort1 [symbol(#let)] /*@ Set membership over terms. In addition to equality over concrete patterns, K also supports computing equality @@ -476,8 +476,8 @@ module K change in the future).*/ syntax Bool ::= left: - K ":=K" K [function, total, klabel(_:=K_), symbol, group(equalEqualK)] - | K ":/=K" K [function, total, klabel(_:/=K_), symbol, group(notEqualEqualK)] + K ":=K" K [function, total, symbol(_:=K_), group(equalEqualK)] + | K ":/=K" K [function, total, symbol(_:/=K_), group(notEqualEqualK)] endmodule // To be used to parse terms in full K @@ -545,7 +545,7 @@ regular K rules to disambiguate as necessary. ```k module K-AMBIGUITIES - syntax {Sort} Sort ::= amb(Sort, Sort) [klabel(amb), symbol] + syntax {Sort} Sort ::= amb(Sort, Sort) [symbol(amb)] endmodule ``` @@ -565,7 +565,7 @@ module K-LOCATIONS imports INT-SYNTAX // filename, startLine, startCol, endLine, endCol - syntax {Sort} Sort ::= #location(Sort, String, Int, Int, Int, Int) [klabel(#location), symbol, format(%3)] + syntax {Sort} Sort ::= #location(Sort, String, Int, Int, Int, Int) [symbol(#location), format(%3)] endmodule ``` diff --git a/k-distribution/include/kframework/builtin/rat.md b/k-distribution/include/kframework/builtin/rat.md index 8ac2ad60058..eb31cc23684 100644 --- a/k-distribution/include/kframework/builtin/rat.md +++ b/k-distribution/include/kframework/builtin/rat.md @@ -32,13 +32,13 @@ You can: ```k syntax Rat ::= left: - Rat "^Rat" Int [function, total, klabel(_^Rat_), symbol, smtlib(ratpow), hook(RAT.pow)] + Rat "^Rat" Int [function, total, symbol(_^Rat_), smtlib(ratpow), hook(RAT.pow)] > left: - Rat "*Rat" Rat [function, total, klabel(_*Rat_), symbol, left, smtlib(ratmul), hook(RAT.mul)] - | Rat "/Rat" Rat [function, klabel(_/Rat_), symbol, left, smtlib(ratdiv), hook(RAT.div)] + Rat "*Rat" Rat [function, total, symbol(_*Rat_), left, smtlib(ratmul), hook(RAT.mul)] + | Rat "/Rat" Rat [function, symbol(_/Rat_), left, smtlib(ratdiv), hook(RAT.div)] > left: - Rat "+Rat" Rat [function, total, klabel(_+Rat_), symbol, left, smtlib(ratadd), hook(RAT.add)] - | Rat "-Rat" Rat [function, total, klabel(_-Rat_), symbol, left, smtlib(ratsub), hook(RAT.sub)] + Rat "+Rat" Rat [function, total, symbol(_+Rat_), left, smtlib(ratadd), hook(RAT.add)] + | Rat "-Rat" Rat [function, total, symbol(_-Rat_), left, smtlib(ratsub), hook(RAT.sub)] ``` Comparison @@ -49,12 +49,12 @@ one of less than, less than or equalto, greater than, or greater than or equal to the other: ```k - syntax Bool ::= Rat "==Rat" Rat [function, total, klabel(_==Rat_), symbol, smtlib(rateq), hook(RAT.eq)] - | Rat "=/=Rat" Rat [function, total, klabel(_=/=Rat_), symbol, smtlib(ratne), hook(RAT.ne)] - | Rat ">Rat" Rat [function, total, klabel(_>Rat_), symbol, smtlib(ratgt), hook(RAT.gt)] - | Rat ">=Rat" Rat [function, total, klabel(_>=Rat_), symbol, smtlib(ratge), hook(RAT.ge)] - | Rat "Rat" Rat [function, total, symbol(_>Rat_), smtlib(ratgt), hook(RAT.gt)] + | Rat ">=Rat" Rat [function, total, symbol(_>=Rat_), smtlib(ratge), hook(RAT.ge)] + | Rat "" 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/checkWarns/symbolKLabel.k b/k-distribution/tests/regression-new/checkWarns/symbolKLabel.k new file mode 100644 index 00000000000..125656ab331 --- /dev/null +++ b/k-distribution/tests/regression-new/checkWarns/symbolKLabel.k @@ -0,0 +1,22 @@ +module SYMBOLKLABEL-SYNTAX +endmodule + +module PW1 + syntax Foo ::= "foo" [klabel(foo), symbol, unused] +endmodule + +module PW2 + syntax Foo ::= "foo" [klabel(foo), unused] +endmodule + +module PW3 + syntax Foo ::= Bar + syntax Foo ::= "foo" Foo [klabel(foo), unused] + syntax Bar ::= "foo" Bar [klabel(foo), unused] +endmodule + +module SYMBOLKLABEL + imports PW1 + imports PW2 + imports PW3 +endmodule diff --git a/k-distribution/tests/regression-new/checkWarns/symbolKLabel.k.out b/k-distribution/tests/regression-new/checkWarns/symbolKLabel.k.out new file mode 100644 index 00000000000..4b227f7a0f0 --- /dev/null +++ b/k-distribution/tests/regression-new/checkWarns/symbolKLabel.k.out @@ -0,0 +1,21 @@ +[Error] Compiler: The zero-argument form of `symbol` is deprecated. Replace `klabel(foo), symbol` by `symbol(foo)`. + Source(symbolKLabel.k) + Location(5,18,5,53) + 5 | syntax Foo ::= "foo" [klabel(foo), symbol, unused] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Error] Compiler: Attribute `klabel(_)` is deprecated. Either remove `klabel(foo)`, or replace it by `symbol(foo)`. + Source(symbolKLabel.k) + Location(9,20,9,47) + 9 | syntax Foo ::= "foo" [klabel(foo), unused] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Error] Compiler: Attribute `klabel(foo) is deprecated, but marks an overload. Add `overload(foo)`. + Source(symbolKLabel.k) + Location(14,20,14,51) + 14 | syntax Foo ::= "foo" Foo [klabel(foo), unused] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Error] Compiler: Attribute `klabel(foo) is deprecated, but marks an overload. Add `overload(foo)`. + Source(symbolKLabel.k) + Location(15,20,15,51) + 15 | syntax Bar ::= "foo" Bar [klabel(foo), unused] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Error] Compiler: Had 4 structural errors. diff --git a/k-distribution/tests/regression-new/checks/invalidSymbol.k b/k-distribution/tests/regression-new/checks/invalidSymbol.k index d538f158b1d..22830c4faa7 100644 --- a/k-distribution/tests/regression-new/checks/invalidSymbol.k +++ b/k-distribution/tests/regression-new/checks/invalidSymbol.k @@ -1,10 +1,10 @@ // Copyright (c) Runtime Verification, Inc. All Rights Reserved. module INVALIDSYMBOL -syntax Foo ::= foo() [klabel(#KToken), symbol] +syntax Foo ::= foo() [symbol(#KToken)] -syntax Bar ::= bar() [klabel(foo), symbol] -syntax Baz ::= baz() [klabel(foo), symbol] +syntax Bar ::= bar() [symbol(foo)] +syntax Baz ::= baz() [symbol(foo)] syntax Exp ::= Val syntax Val ::= "val" diff --git a/k-distribution/tests/regression-new/checks/invalidSymbol.k.out b/k-distribution/tests/regression-new/checks/invalidSymbol.k.out index 4eb9bcc8cc0..162f809923b 100644 --- a/k-distribution/tests/regression-new/checks/invalidSymbol.k.out +++ b/k-distribution/tests/regression-new/checks/invalidSymbol.k.out @@ -1,11 +1,11 @@ -[Error] Compiler: Symbol #KToken is not unique. Previously defined as: syntax KBott ::= "#token" "(" KString "," KString ")" [klabel(#KToken), symbol] +[Error] Compiler: Symbol #KToken is not unique. Previously defined as: syntax KBott ::= "#token" "(" KString "," KString ")" [symbol(#KToken)] Source(invalidSymbol.k) - Location(4,16,4,47) - 4 | syntax Foo ::= foo() [klabel(#KToken), symbol] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -[Error] Compiler: Symbol foo is not unique. Previously defined as: syntax Bar ::= "bar" "(" ")" [klabel(foo), symbol] + Location(4,16,4,39) + 4 | syntax Foo ::= foo() [symbol(#KToken)] + . ^~~~~~~~~~~~~~~~~~~~~~~ +[Error] Compiler: Symbol foo is not unique. Previously defined as: syntax Bar ::= "bar" "(" ")" [symbol(foo)] Source(invalidSymbol.k) - Location(7,16,7,43) - 7 | syntax Baz ::= baz() [klabel(foo), symbol] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(7,16,7,35) + 7 | syntax Baz ::= baz() [symbol(foo)] + . ^~~~~~~~~~~~~~~~~~~ [Error] Compiler: Had 2 structural errors. diff --git a/k-distribution/tests/regression-new/checks/overloadKLabel.k.out b/k-distribution/tests/regression-new/checks/overloadKLabel.k.out index 44d93e75af2..ea40ac2dbc1 100644 --- a/k-distribution/tests/regression-new/checks/overloadKLabel.k.out +++ b/k-distribution/tests/regression-new/checks/overloadKLabel.k.out @@ -1,4 +1,4 @@ -[Error] Compiler: The attributes `klabel(_)` and `overload(_)` may not occur together. +[Error] Compiler: The attributes `klabel` and `overload` may not occur together. Either remove `klabel(_._)`, or replace it by `symbol(_._)` Source(overloadKLabel.k) Location(4,19,4,59) 4 | | Exp "." Id [klabel(_._), overload(_._)] diff --git a/k-distribution/tests/regression-new/checks/paramAmb.k.out b/k-distribution/tests/regression-new/checks/paramAmb.k.out index 114e591aced..ad1e9f23fb5 100644 --- a/k-distribution/tests/regression-new/checks/paramAmb.k.out +++ b/k-distribution/tests/regression-new/checks/paramAmb.k.out @@ -1,9 +1,9 @@ [Error] Inner Parser: Parsing ambiguity. -1: syntax {Sort} Sort ::= Sort "=>" Sort [klabel(#KRewrite), symbol] +1: syntax {Sort} Sort ::= Sort "=>" Sort [symbol(#KRewrite)] #KRewrite(#SemanticCastToA(#token("X","#KVariable")),`label(_,_)_PARAMAMB_KItem_N_T`(#SemanticCastToA(#token("X","#KVariable")),`wrap__PARAMAMB_T_M`(#SemanticCastToA(#token("X","#KVariable"))))) -2: syntax {Sort} Sort ::= Sort "=>" Sort [klabel(#KRewrite), symbol] +2: syntax {Sort} Sort ::= Sort "=>" Sort [symbol(#KRewrite)] #KRewrite(#SemanticCastToB(#token("X","#KVariable")),`label(_,_)_PARAMAMB_KItem_N_T`(#SemanticCastToB(#token("X","#KVariable")),`wrap__PARAMAMB_T_M`(#SemanticCastToB(#token("X","#KVariable"))))) -3: syntax {Sort} Sort ::= Sort "=>" Sort [klabel(#KRewrite), symbol] +3: syntax {Sort} Sort ::= Sort "=>" Sort [symbol(#KRewrite)] #KRewrite(#SemanticCastToX(#token("X","#KVariable")),`label(_,_)_PARAMAMB_KItem_N_T`(#SemanticCastToX(#token("X","#KVariable")),`wrap__PARAMAMB_T_X`(#SemanticCastToX(#token("X","#KVariable"))))) Source(paramAmb.k) Location(12,8,12,29) 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/context-labels/context-spec.k.out b/k-distribution/tests/regression-new/context-labels/context-spec.k.out index f2a5520f2a1..bae1a0cf828 100644 --- a/k-distribution/tests/regression-new/context-labels/context-spec.k.out +++ b/k-distribution/tests/regression-new/context-labels/context-spec.k.out @@ -7,7 +7,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): Lbl'-LT-'k'-GT-'{}( kseq{}( /* Inj: */ inj{SortA{}, SortKItem{}}( - Lblfoo'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A{}( + Lblfoo{}( Lbla'Unds'CONTEXT'Unds'A{}(), Lbla'Unds'CONTEXT'Unds'A{}() ) @@ -37,7 +37,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): Lbla'Unds'CONTEXT'Unds'A{}() ), kseq{}( - Lbl'Hash'freezerfoo'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A0'Unds'{}( + Lbl'Hash'freezerfoo0'Unds'{}( kseq{}( /* Inj: */ inj{SortA{}, SortKItem{}}( Lbla'Unds'CONTEXT'Unds'A{}() @@ -71,7 +71,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): \dv{SortInt{}}("0") ), kseq{}( - Lbl'Hash'freezerfoo'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A0'Unds'{}( + Lbl'Hash'freezerfoo0'Unds'{}( kseq{}( /* Inj: */ inj{SortA{}, SortKItem{}}( Lbla'Unds'CONTEXT'Unds'A{}() @@ -102,7 +102,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): Lbl'-LT-'k'-GT-'{}( kseq{}( /* Inj: */ inj{SortA{}, SortKItem{}}( - Lblfoo'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A{}( + Lblfoo{}( /* Inj: */ inj{SortInt{}, SortA{}}( \dv{SortInt{}}("0") ), @@ -134,7 +134,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): Lbla'Unds'CONTEXT'Unds'A{}() ), kseq{}( - Lbl'Hash'freezerfoo'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A1'Unds'{}( + Lbl'Hash'freezerfoo1'Unds'{}( kseq{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") @@ -168,7 +168,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): \dv{SortInt{}}("0") ), kseq{}( - Lbl'Hash'freezerfoo'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A1'Unds'{}( + Lbl'Hash'freezerfoo1'Unds'{}( kseq{}( /* Inj: */ inj{SortInt{}, SortKItem{}}( \dv{SortInt{}}("0") @@ -391,7 +391,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): Lbl'-LT-'k'-GT-'{}( kseq{}( /* Inj: */ inj{SortA{}, SortKItem{}}( - Lblbaz'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A{}( + Lblbaz{}( Lbla'Unds'CONTEXT'Unds'A{}(), Lbla'Unds'CONTEXT'Unds'A{}() ) @@ -421,7 +421,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): Lbla'Unds'CONTEXT'Unds'A{}() ), kseq{}( - Lbl'Hash'freezerbaz'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A1'Unds'{}( + Lbl'Hash'freezerbaz1'Unds'{}( kseq{}( /* Inj: */ inj{SortA{}, SortKItem{}}( Lbla'Unds'CONTEXT'Unds'A{}() @@ -455,7 +455,7 @@ kore-repl: Debug (DebugAppliedLabeledRewriteRule): \dv{SortInt{}}("0") ), kseq{}( - Lbl'Hash'freezerbaz'LParUndsCommUndsRParUnds'CONTEXT'Unds'A'Unds'A'Unds'A1'Unds'{}( + Lbl'Hash'freezerbaz1'Unds'{}( kseq{}( /* Inj: */ inj{SortA{}, SortKItem{}}( Lbla'Unds'CONTEXT'Unds'A{}() diff --git a/k-distribution/tests/regression-new/context-labels/context.k b/k-distribution/tests/regression-new/context-labels/context.k index 37a68c1dcc4..9dcef35742a 100644 --- a/k-distribution/tests/regression-new/context-labels/context.k +++ b/k-distribution/tests/regression-new/context-labels/context.k @@ -5,9 +5,9 @@ module CONTEXT syntax KResult ::= Int syntax A ::= "a" | Int - | foo( A, A ) [seqstrict, klabel(foo)] + | foo( A, A ) [seqstrict, symbol(foo)] | bar( A, A ) - | baz( A, A ) [strict(2), klabel(baz)] + | baz( A, A ) [strict(2), symbol(baz)] context [bar1]: bar( HOLE, _ ) context [bar2]: bar( _, HOLE ) 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-1760/test.k.out b/k-distribution/tests/regression-new/issue-1760/test.k.out index 98dcbb73cf5..6e538da1617 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,135) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,127) + 21 | | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(test.k) - 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`(_,_) + Location(22,19,22,133) + 22 | > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Warning] Compiler: Non exhaustive match detected: `_orKat_`(_,_) Source(test.k) Location(23,19,23,130) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + 23 | | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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/issue-999/kat.k.out b/k-distribution/tests/regression-new/issue-999/kat.k.out index d4a92c54985..b351a023b04 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,135) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,127) + 21 | | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(kat.k) - 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`(_,_) + Location(22,19,22,133) + 22 | > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Warning] Compiler: Non exhaustive match detected: `_orKat_`(_,_) Source(kat.k) Location(23,19,23,130) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + 23 | | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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 7c55495b60f..e57e7c5018b 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/proof-instrumentation-debug/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out index 0bc6c9ed61a..e85e8142c6f 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out differ diff --git a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out index 88097b81433..b1ec2ff4c13 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out differ 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) diff --git a/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java index 0bf8af0b12f..8268041cca9 100644 --- a/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -343,21 +343,64 @@ private void checkLatex(Production prod) { } private void checkSymbolKLabel(Production prod) { - if (prod.att().contains(Att.SYMBOL()) && prod.att().contains(Att.KLABEL())) { - if (!prod.att().get(Att.SYMBOL()).isEmpty()) { + if (!prod.att().contains(Att.KLABEL())) { + return; + } + + var kLabelValue = prod.att().get(Att.KLABEL()); + + if (prod.att().contains(Att.SYMBOL())) { + if (prod.att().get(Att.SYMBOL()).isEmpty()) { + var message = + "The zero-argument form of `symbol` is deprecated. Replace `klabel(" + + kLabelValue + + "), symbol` by `symbol(" + + kLabelValue + + ")`."; + + kem.registerCompilerWarning(ExceptionType.FUTURE_ERROR, errors, message, prod); + } else { errors.add( KEMException.compilerError( "The 1-argument form of the `symbol(_)` attribute cannot be combined with `klabel(_)`.", prod)); } + } else { + var overloadProds = m.overloads().elements(); + + if (overloadProds.contains(prod)) { + var message = + "Attribute `klabel(" + + kLabelValue + + ") is deprecated, but marks an overload. Add `overload(" + + kLabelValue + + ")`."; + + kem.registerCompilerWarning(ExceptionType.FUTURE_ERROR, errors, message, prod); + } else { + var message = + "Attribute `klabel(_)` is deprecated. Either remove `klabel(" + + kLabelValue + + ")`, or replace it by `symbol(" + + kLabelValue + + ")`."; + + kem.registerCompilerWarning(ExceptionType.FUTURE_ERROR, errors, message, prod); + } } } private void checkKLabelOverload(Production prod) { if (prod.att().contains(Att.KLABEL()) && prod.att().contains(Att.OVERLOAD())) { - errors.add( - KEMException.compilerError( - "The attributes `klabel(_)` and `overload(_)` may not occur together.", prod)); + var klabelKey = prod.att().get(Att.KLABEL()); + var msg = + "The attributes `klabel` and `overload` may not occur together. Either remove `klabel(" + + klabelKey + + ")`, or replace it by `symbol(" + + klabelKey + + ")`"; + + errors.add(KEMException.compilerError(msg, prod)); } } diff --git a/pyk/regression-new/bison-glr-bug/iele.k b/pyk/regression-new/bison-glr-bug/iele.k index b60877c2e2e..e6986d1d1eb 100644 --- a/pyk/regression-new/bison-glr-bug/iele.k +++ b/pyk/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 ::= @@ -307,7 +307,7 @@ module IELE-COMMON syntax ContractDeclaration ::= "external" "contract" IeleName syntax GlobalDefinition ::= - GlobalName "=" IntConstant [klabel(globalDefinition)] + GlobalName "=" IntConstant [symbol(globalDefinition)] syntax FunctionSignature ::= GlobalName "(" FunctionParameters ")" syntax FunctionParameters ::= diff --git a/pyk/regression-new/checkWarns/missingKlabel.k b/pyk/regression-new/checkWarns/missingKlabel.k index 4ce27642627..7ec6dbbb179 100644 --- a/pyk/regression-new/checkWarns/missingKlabel.k +++ b/pyk/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/pyk/regression-new/issue-1273/test.k b/pyk/regression-new/issue-1273/test.k index 28d7244cd37..482aae99003 100644 --- a/pyk/regression-new/issue-1273/test.k +++ b/pyk/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/pyk/regression-new/issue-1760/test.k b/pyk/regression-new/issue-1760/test.k index 7fc1b087108..0be7ed1a953 100644 --- a/pyk/regression-new/issue-1760/test.k +++ b/pyk/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/pyk/regression-new/issue-1760/test.k.out b/pyk/regression-new/issue-1760/test.k.out index 98dcbb73cf5..6e538da1617 100644 --- a/pyk/regression-new/issue-1760/test.k.out +++ b/pyk/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,135) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,127) + 21 | | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(test.k) - 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`(_,_) + Location(22,19,22,133) + 22 | > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Warning] Compiler: Non exhaustive match detected: `_orKat_`(_,_) Source(test.k) Location(23,19,23,130) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + 23 | | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/pyk/regression-new/issue-1879-kproveTrans/haskell/test.k b/pyk/regression-new/issue-1879-kproveTrans/haskell/test.k index 12594e4fbcb..5dcbc869e0f 100644 --- a/pyk/regression-new/issue-1879-kproveTrans/haskell/test.k +++ b/pyk/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/pyk/regression-new/issue-999/kat.k b/pyk/regression-new/issue-999/kat.k index ad420232c57..6ec30457d33 100644 --- a/pyk/regression-new/issue-999/kat.k +++ b/pyk/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/pyk/regression-new/issue-999/kat.k.out b/pyk/regression-new/issue-999/kat.k.out index d4a92c54985..b351a023b04 100644 --- a/pyk/regression-new/issue-999/kat.k.out +++ b/pyk/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,135) - 21 | | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)] - . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Location(21,19,21,127) + 21 | | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ [Warning] Compiler: Non exhaustive match detected: `_andKat_`(_,_) Source(kat.k) - 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`(_,_) + Location(22,19,22,133) + 22 | > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)] + . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[Warning] Compiler: Non exhaustive match detected: `_orKat_`(_,_) Source(kat.k) Location(23,19,23,130) - 23 | | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] + 23 | | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)] . ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/pyk/regression-new/unparseKORE/test.k b/pyk/regression-new/unparseKORE/test.k index f57646f8187..51fed8939bf 100644 --- a/pyk/regression-new/unparseKORE/test.k +++ b/pyk/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) diff --git a/pyk/src/pyk/konvert/_module_to_kore.py b/pyk/src/pyk/konvert/_module_to_kore.py index 3b5d65432b9..d87ec49e461 100644 --- a/pyk/src/pyk/konvert/_module_to_kore.py +++ b/pyk/src/pyk/konvert/_module_to_kore.py @@ -877,11 +877,16 @@ def _update(syntax_sort: KSyntaxSort, concat_atts: Mapping[KSort, KAtt]) -> KSyn assert syntax_sort.sort in concat_atts concat_att = concat_atts[syntax_sort.sort] + # Workaround until zero-argument symbol is removed, rather than + # deprecated. + symbol = concat_att[Atts.SYMBOL] + assert symbol is not None + return syntax_sort.let( att=syntax_sort.att.update( [ # TODO Here, the attriubte is stored as dict, but ultimately we should parse known attributes in KAtt.from_dict - Atts.CONCAT(KApply(concat_att[Atts.KLABEL]).to_dict()), + Atts.CONCAT(KApply(symbol).to_dict()), # TODO Here, we keep the format from the frontend so that the attributes on SyntaxSort and Production are of the same type. Atts.ELEMENT(concat_att[Atts.ELEMENT]), Atts.UNIT(concat_att[Atts.UNIT]), diff --git a/pyk/src/tests/integration/test_kompile.py b/pyk/src/tests/integration/test_kompile.py index 3491531f22d..b702982cdbc 100644 --- a/pyk/src/tests/integration/test_kompile.py +++ b/pyk/src/tests/integration/test_kompile.py @@ -65,21 +65,19 @@ def test_booster_kompile(tmp_path: Path) -> None: assert DefinitionInfo(output_dir / 'llvm-library').backend == KompileBackend.LLVM -class TestKLabel(KompiledTest): +class TestSymbol(KompiledTest): KOMPILE_DEFINITION = """ - module KLABEL + module SYMBOL syntax Foo ::= "foo" [symbol(foo)] - | "bar" [klabel(bar), symbol] - | "baz" [klabel(baz)] | "qux" endmodule """ - KOMPILE_MAIN_MODULE = 'KLABEL' - KOMPILE_ARGS = {'syntax_module': 'KLABEL'} + KOMPILE_MAIN_MODULE = 'SYMBOL' + KOMPILE_ARGS = {'syntax_module': 'SYMBOL'} def test(self, definition: KDefinition) -> None: # Given - module = definition.module('KLABEL') + module = definition.module('SYMBOL') def klabel_defined_at_line(line: int) -> KLabel: (prod,) = (prod for prod in module.productions if prod.att.get(Atts.LOCATION, [None])[0] == line) @@ -88,15 +86,11 @@ def klabel_defined_at_line(line: int) -> KLabel: return res foo = klabel_defined_at_line(2) - bar = klabel_defined_at_line(3) - baz = klabel_defined_at_line(4) - qux = klabel_defined_at_line(5) + qux = klabel_defined_at_line(3) # Then assert foo.name == 'foo' - assert bar.name == 'bar' - assert baz.name == 'baz_KLABEL_Foo' - assert qux.name == 'qux_KLABEL_Foo' + assert qux.name == 'qux_SYMBOL_Foo' class TestSubsortSymbol(KompiledTest):