Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Deprecate symbol and klabel #4045

Merged
merged 23 commits into from
Jul 4, 2024
Merged

Deprecate symbol and klabel #4045

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
48ab50b
PW1: implement warning
Baltoli Feb 26, 2024
6478f8e
PW1: fix standard library
Baltoli Feb 26, 2024
2495800
Fix regression tests
Baltoli Feb 26, 2024
32f7a5e
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Mar 14, 2024
4cb05fe
Implement PW2, PW3
Baltoli Mar 14, 2024
be26317
Fix missing case in domains.md
Baltoli Mar 14, 2024
a67ce8f
Update regression tests
Baltoli Mar 14, 2024
3bb8c65
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Mar 21, 2024
6c756eb
Update pushList symbol
Baltoli Mar 21, 2024
61a9427
Implement test for warnings
Baltoli Mar 21, 2024
827ff45
Update warning for klabel, overload
Baltoli Mar 21, 2024
a053301
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Mar 26, 2024
3457cb6
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Mar 27, 2024
81ac0bb
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Mar 27, 2024
c28f891
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Mar 28, 2024
3c5dc81
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Jul 2, 2024
4bb1bf1
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Jul 3, 2024
306d6e5
Fix module-to-kore tests
Baltoli Jul 3, 2024
5b09f79
Fix regression tests
Baltoli Jul 3, 2024
e52fbff
Type checker
Baltoli Jul 3, 2024
b090f3f
Update proof test
Baltoli Jul 3, 2024
60ad675
Update proof test
Baltoli Jul 3, 2024
97dfaa8
Merge branch 'develop' into deprecate-symbol-klabel
Baltoli Jul 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
306 changes: 153 additions & 153 deletions k-distribution/include/kframework/builtin/domains.md
View file
Open in desktop

Large diffs are not rendered by default.

50 changes: 25 additions & 25 deletions k-distribution/include/kframework/builtin/ffi.md
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading