Replace usages of priorities, require, and import (#4026)

Part of #4009

Replace usages of deprecated tokens:
- `syntax priorities` with `syntax priority`
- `require` with `requires`
- `import` with `imports`

The outer parser is unchanged and still accepts the deprecated tokens -
this is just an initial PR to clean up all the usages in various test
files.

docs/user_manual.md

@@ -360,7 +360,7 @@ string, which serves as a unique internal identifier and also is used in kast
 format of that syntax. If we need to reference a certain syntax production
 externally, we have to manually define the klabels using the `klabel` attribute.
 One example of where you would want to do this is to be able to refer to a given
-symbol via the `syntax priorities` attribute, or to enable overloading of a
+symbol via the `syntax priority` attribute, or to enable overloading of a
 given symbol.
 
 If you only provide the `klabel` attribute, you can use the provided `klabel` to
@@ -810,7 +810,7 @@ modularity. As a result, it becomes infeasible to declare priority and
 associativity inline within a set of productions, because the productions
 are not contiguous within a single file.
 
-For this purpose, we introduce the equivalent `syntax priorities`,
+For this purpose, we introduce the equivalent `syntax priority`,
 `syntax left`, `syntax right`, and `syntax non-assoc` declarations. For
 example, the above grammar can be written equivalently as:
 
@@ -820,7 +820,7 @@ syntax Exp ::= Exp "*" Exp [group(mult)]
              | Exp "+" Exp [group(add)]
              | Exp "-" Exp [group(sub)]
 
-syntax priorities mult div > add sub
+syntax priority mult div > add sub
 syntax left mult div
 syntax right add sub
 ```
@@ -836,15 +836,15 @@ syntax Exp ::= Exp "*" Exp [group(mult)]
              | Exp "+" Exp [group(add)]
              | Exp "-" Exp [group(add)]
 
-syntax priorities mult > add
+syntax priority mult > add
 syntax left mult
 syntax right add
 ```
 
 Note that `syntax [left|right|non-assoc]` should not be used to group together
 productions with different priorities. For example, this code would be invalid:
 ```k
-syntax priorities mult > add
+syntax priority mult > add
 syntax left mult add
 ```
 

k-distribution/include/kframework/builtin/domains.md

@@ -17,7 +17,7 @@ function on an undefined input, the behavior is undefined. In particular, when
 this happens, interpreters generated by the K LLVM backend may crash.
 
 ```k
-require "kast.md"
+requires "kast.md"
 ```
 
 Default Modules
@@ -256,7 +256,7 @@ left and the value is on the right.
 ```k
   syntax Map ::= KItem "|->" KItem                      [function, total, hook(MAP.element), klabel(_|->_), symbol, injective]
 
-  syntax priorities _|->_ > _Map_ .Map
+  syntax priority _|->_ > _Map_ .Map
   syntax non-assoc _|->_
 ```
 
@@ -524,7 +524,7 @@ 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 priorities _r|->_ > _RangeMap_ .RangeMap
+  syntax priority _r|->_ > _RangeMap_ .RangeMap
   syntax non-assoc _r|->_
 ```
 
@@ -2277,15 +2277,15 @@ module K-EQUAL-SYNTAX
                   K "==K" K           [function, total, comm, smt-hook(=), hook(KEQUAL.eq), klabel(_==K_), symbol, group(equalEqualK)]
                 | K "=/=K" K          [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, group(notEqualEqualK)]
 
-  syntax priorities equalEqualK notEqualEqualK > boolOperation mlOp
+  syntax priority equalEqualK notEqualEqualK > boolOperation mlOp
 
   syntax {Sort} Sort ::= "#if" Bool "#then" Sort "#else" Sort "#fi" [function, total, symbol(ite), smt-hook(ite), hook(KEQUAL.ite)]
 
 endmodule
 
 module K-EQUAL-KORE [symbolic]
-  import private BOOL
-  import K-EQUAL-SYNTAX
+  imports private BOOL
+  imports K-EQUAL-SYNTAX
 
   rule K1:Bool ==K K2:Bool => K1 ==Bool K2 [simplification]
   rule {K1 ==K K2 #Equals true} => {K1 #Equals K2} [simplification]
@@ -2300,9 +2300,9 @@ module K-EQUAL-KORE [symbolic]
 endmodule
 
 module K-EQUAL
-  import private BOOL
-  import K-EQUAL-SYNTAX
-  import K-EQUAL-KORE
+  imports private BOOL
+  imports K-EQUAL-SYNTAX
+  imports K-EQUAL-KORE
 
   rule K1:K =/=K K2:K => notBool (K1 ==K K2)
 

k-distribution/include/kframework/builtin/ffi.md

@@ -18,7 +18,7 @@ to memory corruption in your interpreter and can cause segmentation faults or
 corrupted term representations that lead to undefined behavior at runtime.
 
 ```k
-require "domains.md"
+requires "domains.md"
 
 module FFI-SYNTAX
   imports private LIST

k-distribution/include/kframework/builtin/kast.md

@@ -144,13 +144,13 @@ module ML-SYNTAX [not-lr1]
                                 | "#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 priorities mlUnary > mlEquals > mlAnd
+  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 priorities mlImplies > mlQuantifier
+  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)]

k-distribution/include/kframework/builtin/prelude.md

@@ -16,6 +16,6 @@ with `kompile -E`, or if you wish to modify the inner syntax of K by providing
 your own version of these files with different syntax.
 
 ```k
-require "kast.md"
-require "domains.md"
+requires "kast.md"
+requires "domains.md"
 ```

k-distribution/include/kframework/builtin/unification.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "domains.md"
+requires "domains.md"
 module UNIFICATION
   imports SET
 

k-distribution/k-tutorial/1_basic/04_disambiguation/README.md

@@ -207,7 +207,7 @@ module LESSON-04-D
                    | Boolean "^" Boolean [group(xor), function]
                    | Boolean "||" Boolean [group(or), function]
 
-  syntax priorities literal atom > not > and > xor > or
+  syntax priority literal atom > not > and > xor > or
   syntax left and
   syntax left xor
   syntax left or
@@ -216,13 +216,13 @@ endmodule
 
 This introduces a couple of new features of K. First, the `group(_)` attribute
 is used to conceptually group together sets of sentences under a common
-user-defined name. For example, `literal` in the `syntax priorities` sentence is
+user-defined name. For example, `literal` in the `syntax priority` sentence is
 used to refer to all the productions marked with the `group(literal)` attribute,
 i.e., `true` and `false`. A production can belong to multiple groups using
 syntax such as `group(myGrp1,myGrp2)`.
 
 Once we understand this, it becomes relatively straightforward to understand
-the meaning of this grammar. Each `syntax priorities` sentence defines a
+the meaning of this grammar. Each `syntax priority` sentence defines a
 priority relation where `>` separates different priority groups. Each priority
 group is defined by a list of one or more group names, and consists of all
 productions which are members of at least one of those named groups.

k-distribution/src/test/resources/compiler-tests/assoc-test.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "domains.md"
+requires "domains.md"
 
 module ASSOC-TEST
   imports INT

k-distribution/src/test/resources/convertor-tests/configuration-kilexpected.k

@@ -1,7 +1,7 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
 DEF: null -> null
-require "include.k"
+requires "include.k"
 module INCLUDE
   syntax #Bool ::= "false"
 

k-distribution/src/test/resources/convertor-tests/configuration.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "include.k"
+requires "include.k"
 
 module TEST
   imports INCLUDE

k-distribution/src/test/resources/convertor-tests/context.k

@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "include.k"
+requires "include.k"
 
 module TEST
   imports INCLUDE

k-distribution/src/test/resources/convertor-tests/imp_lesson1.k

@@ -1,10 +1,10 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module IMP-SYNTAX
-  import ID
-  import INT
-  import BOOL
+  imports ID
+  imports INT
+  imports BOOL
 
   syntax AExp  ::= Int | Id
                  | AExp "/" AExp              [left, strict]

k-distribution/src/test/resources/convertor-tests/imp_lesson2.k

@@ -1,10 +1,10 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module IMP-SYNTAX
-  import ID
-  import INT
-  import BOOL
+  imports ID
+  imports INT
+  imports BOOL
 
   syntax AExp  ::= Int | Id
                  | AExp "/" AExp              [left, strict]
@@ -30,7 +30,7 @@ endmodule
 
 module IMP
   imports IMP-SYNTAX
-  import MAP
+  imports MAP
   syntax KResult ::= Int | Bool
 
   configuration <T color="yellow">

k-distribution/src/test/resources/convertor-tests/kore_varlabel.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "domains.md"
+requires "domains.md"
 
 module VARLABEL-SYNTAX
 

k-distribution/src/test/resources/convertor-tests/simpleNestedConfiguration.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module FUNC
     syntax Foo ::= "foo"

k-distribution/src/test/resources/convertor-tests/simpleNestedFunctions.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module FUNC
     syntax Foo ::= "foo" Bar    [klabel(foo), function]

k-distribution/src/test/resources/convertor-tests/syntaxPriorities-kilexpected.k

@@ -15,7 +15,7 @@ module TEST
 
   syntax left t m
 
-  syntax prioritiesx
+  syntax priorityx
 > y z
 > t m
 > u

k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities-kilexpected.k

@@ -13,7 +13,7 @@ module TEST
 
   syntax left x
 
-  syntax prioritiesx
+  syntax priorityx
 > y z
 > t
 > u

k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities.k

@@ -7,7 +7,7 @@ module TEST
                | "t"    [andanohter]
                | "u"    [off]
 
-  syntax priorities x > y z > t > u
+  syntax priority x > y z > t > u
   syntax left x
   syntax right y
 endmodule

k-distribution/tests/profiling/elrond-semantics/test.k

@@ -2188,7 +2188,7 @@ module MAP-BYTES-TO-BYTES
     ".MapBytesToBytes" [function, hook(MAP.unit), klabel(.MapBytesToBytes), symbol, total]
   syntax MapBytesToBytes  ::=
     WrappedBytes "Bytes2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Bytes2Bytes|->_), symbol, total]
-  syntax priorities _Bytes2Bytes|->_  > _MapBytesToBytes_ .MapBytesToBytes
+  syntax priority _Bytes2Bytes|->_  > _MapBytesToBytes_ .MapBytesToBytes
   syntax non-assoc _Bytes2Bytes|->_
   syntax WrappedBytes  ::=
     MapBytesToBytes "[" WrappedBytes "]" [function, hook(MAP.lookup), klabel(MapBytesToBytes:lookup), symbol]
@@ -2570,7 +2570,7 @@ module MAP-INT-TO-BYTES
     ".MapIntToBytes" [function, hook(MAP.unit), klabel(.MapIntToBytes), symbol, total]
   syntax MapIntToBytes  ::=
     WrappedInt "Int2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Int2Bytes|->_), symbol, total]
-  syntax priorities _Int2Bytes|->_  > _MapIntToBytes_ .MapIntToBytes
+  syntax priority _Int2Bytes|->_  > _MapIntToBytes_ .MapIntToBytes
   syntax non-assoc _Int2Bytes|->_
   syntax WrappedBytes  ::=
     MapIntToBytes "[" WrappedInt "]" [function, hook(MAP.lookup), klabel(MapIntToBytes:lookup), symbol]

k-distribution/tests/regression-new/append/test.k

@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEAL-SYNTAX
-  import INT-SYNTAX
+  imports INT-SYNTAX
 endmodule
 
 module TEST-SYNTAX

k-distribution/tests/regression-new/bracket-priority/test.k

@@ -13,6 +13,6 @@ syntax BuiltinName ::= "+"
 
 rule (+ I1:Int I2:Int) => I1 +Int I2
 
-syntax priorities defaultBracket > expList
+syntax priority defaultBracket > expList
 
 endmodule

k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "ffi.k"
+requires "ffi.k"
 
 module REQUIREBUILTINK-SYNTAX
 endmodule

k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k.out

@@ -1,5 +1,5 @@
 [Error] Compiler: Requiring a K file in the K builtin directory via a deprecated filename. Please replace "ffi.k" with "ffi.md".
 	Source(requireBuiltinK.k)
-	Location(2,1,2,16)
-	2 |	require "ffi.k"
-	  .	^~~~~~~~~~~~~~~
+	Location(2,1,2,17)
+	2 |	requires "ffi.k"
+	  .	^~~~~~~~~~~~~~~~

k-distribution/tests/regression-new/checks/binder.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "substitution.md"
+requires "substitution.md"
 
 module BINDER
   imports KVAR

k-distribution/tests/regression-new/checks/checkUndeclaredTags.k

@@ -1,4 +1,4 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEST
-  syntax priorities a > b
+  syntax priority a > b
 endmodule

k-distribution/tests/regression-new/checks/checkUndeclaredTags.k.out

@@ -1,5 +1,5 @@
 [Error] Outer Parser: Could not find any productions for tag: a
 	Source(checkUndeclaredTags.k)
-	Location(3,3,3,26)
-	3 |	  syntax priorities a > b
-	  .	  ^~~~~~~~~~~~~~~~~~~~~~~
+	Location(3,3,3,24)
+	3 |	  syntax priority a > b
+	  .	  ^~~~~~~~~~~~~~~~~~~~~

k-distribution/tests/regression-new/checks/missingKResult.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "substitution.md"
+requires "substitution.md"
 
 module MISSINGKRESULT
   imports DOMAINS

k-distribution/tests/regression-new/domains-lemmas-no-smt/domains-lemmas-no-smt.k

@@ -2,7 +2,7 @@
 requires "domains.md"
 
 module DOMAINS-LEMMAS-NO-SMT
-    import INT
+    imports INT
 
     configuration <k> $PGM:Pgm </k>
 

k-distribution/tests/regression-new/issue-1186/test.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "substitution.md"
+requires "substitution.md"
 
 module TEST
   imports KVAR

k-distribution/tests/regression-new/issue-1573/test.k

@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEST
-  import INT
+  imports INT
 
   syntax IntList ::= List{Int, ""}