Skip to content

Commit

Permalink
Deprecate symbol and klabel (#4045)
Browse files Browse the repository at this point in the history 
This PR implements @tothtamas28's warning messages for usages of the
deprecated `klabel(_)` and `symbol` attributes (which can now be
unambiguously replaced by `symbol(_)` and `overload(_)`).

The actual code changes are pretty minimal, but we need to do a bunch of
updates on test cases and related output to keep tests passing.
Additionally, we have pre-merged downstream PRs to make sure other
projects are not subjected to noisy compiler output as a result of
making this change:

Downstream updates:
- [x] C https://github.com/runtimeverification/c-semantics/pull/1125
- [x] EVM runtimeverification/evm-semantics#2378
- [x] WASM
runtimeverification/wasm-semantics#666
- [x] MX Backend
runtimeverification/mx-semantics#298
- [x] Kasmer
runtimeverification/kasmer-multiversx#168
- [x] MIR (new semantics doesn't use `klabel`)
- [x] Pyk (this PR, now that K and Pyk are merged)
- [x] Blockchain Plugin
runtimeverification/blockchain-k-plugin#184
  • Loading branch information
@Baltoli
Baltoli authored Jul 4, 2024
1 parent 10e295c commit 9941e87
Show file tree
Hide file tree
Showing 41 changed files with 481 additions and 396 deletions.
306 changes: 153 additions & 153 deletions k-distribution/include/kframework/builtin/domains.md
View file

Large diffs are not rendered by default.

50 changes: 25 additions & 25 deletions k-distribution/include/kframework/builtin/ffi.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions k-distribution/include/kframework/builtin/json.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
```

Expand Down
106 changes: 53 additions & 53 deletions k-distribution/include/kframework/builtin/kast.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,28 +76,28 @@ 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]
| #LowerId [token]
| 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
// To be used when parsing/pretty-printing ground configurations
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
Expand Down Expand Up @@ -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
```

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 ::= "<top>" #OptionalDots K #OptionalDots "</top>" [klabel(<top>)]
//syntax Cell ::= "<top>" #OptionalDots K #OptionalDots "</top>" [symbol(<top>)]
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,
Expand All @@ -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 ::= "<generatedCounter>" Int "</generatedCounter>" [cell, klabel(<generatedCounter>), symbol, internal]
syntax GeneratedCounterCell ::= "<generatedCounter>" Int "</generatedCounter>" [cell, symbol(<generatedCounter>), internal]
endmodule
```

Expand All @@ -309,12 +309,12 @@ module CONFIG-CELLS
| #LowerId [token]
| #UpperId [token]
syntax Cell ::= "<" #CellName #CellProperties ">" K "</" #CellName ">" [klabel(#configCell), symbol]
syntax Cell ::= "<" #CellName "/>" [klabel(#externalCell), symbol]
syntax Cell ::= "<" #CellName #CellProperties ">" K "</" #CellName ">" [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
```

Expand Down Expand Up @@ -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
```

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
```
Expand All @@ -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
```
26 changes: 13 additions & 13 deletions k-distribution/include/kframework/builtin/rat.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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, klabel(_<Rat_), symbol, smtlib(ratlt), hook(RAT.lt)]
| Rat "<=Rat" Rat [function, total, klabel(_<=Rat_), symbol, smtlib(ratle), hook(RAT.le)]
syntax Bool ::= Rat "==Rat" Rat [function, total, symbol(_==Rat_), smtlib(rateq), hook(RAT.eq)]
| Rat "=/=Rat" Rat [function, total, symbol(_=/=Rat_), smtlib(ratne), hook(RAT.ne)]
| 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 "<Rat" Rat [function, total, symbol(_<Rat_), smtlib(ratlt), hook(RAT.lt)]
| Rat "<=Rat" Rat [function, total, symbol(_<=Rat_), smtlib(ratle), hook(RAT.le)]
```

Min/Max
Expand All @@ -63,8 +63,8 @@ Min/Max
You can compute the minimum and maximum of two rational numbers:

```k
syntax Rat ::= minRat(Rat, Rat) [function, total, klabel(minRat), symbol, smtlib(ratmin), hook(RAT.min)]
| maxRat(Rat, Rat) [function, total, klabel(maxRat), symbol, smtlib(ratmax), hook(RAT.max)]
syntax Rat ::= minRat(Rat, Rat) [function, total, symbol(minRat), smtlib(ratmin), hook(RAT.min)]
| maxRat(Rat, Rat) [function, total, symbol(maxRat), smtlib(ratmax), hook(RAT.max)]
```

Conversion to Floating Point
Expand Down
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/bison-glr-bug/iele.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ::=
Expand Down
4 changes: 2 additions & 2 deletions k-distribution/tests/regression-new/checkWarns/missingKlabel.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
]

Expand Down
Loading

0 comments on commit 9941e87

Please sign in to comment.