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

Scott-Guest · web-flow · commit 1910fe4f8795 · 2024-02-22T03:25:27.000-07:00
Part of runtimeverification/k#4009 Replace usages of deprecated tokens: - `syntax priorities` with `syntax priority` - `require` with `requires` - `import` with `imports`
diff --git a/design-decisions/2020-02-06-One-Path-Deterministic.md b/design-decisions/2020-02-06-One-Path-Deterministic.md
@@ -55,7 +55,7 @@ lead to claims not being proved because the semantics has chosen the wrong path
 Given the following definition:
 ```
 module PATH
-  import DOMAINS
+  imports DOMAINS
   syntax S ::= "a" | "b" | "c"
 
   rule a => b
@@ -71,7 +71,7 @@ if the prover selects to advance the execution using the other rule.
 Given the following definition:
 ```
 module PATH
-  import DOMAINS
+  imports DOMAINS
   syntax S ::= "a" | "b" | "c" 
   syntax Cmd ::= "select"
 
diff --git a/test/all-path/00-basic/01-one-rule/path.k b/test/all-path/00-basic/01-one-rule/path.k
@@ -1,6 +1,6 @@
 module PATH
-  import BOOL
-  import INT
+  imports BOOL
+  imports INT
   syntax S ::= "a" | "b" | "c"
 
   rule a => b
diff --git a/test/all-path/00-basic/02-cyclic-rule/path.k b/test/all-path/00-basic/02-cyclic-rule/path.k
@@ -5,8 +5,8 @@
  *
  */
 module PATH
-  import BOOL
-  import INT
+  imports BOOL
+  imports INT
   syntax S ::= "a" | "b" | "c"
 
   rule a => a
diff --git a/test/all-path/00-basic/03-concurrent-rules/path.k b/test/all-path/00-basic/03-concurrent-rules/path.k
@@ -1,6 +1,6 @@
 module PATH
-  import BOOL
-  import INT
+  imports BOOL
+  imports INT
   syntax S ::= "a" | "b" | "c"
 
   rule a => b
diff --git a/test/all-path/00-basic/04-different-length/path.k b/test/all-path/00-basic/04-different-length/path.k
@@ -1,5 +1,5 @@
 module PATH
-  import BOOL
+  imports BOOL
   syntax S ::= "a" | "b" | "c" | "d" | "e" | "f"
 
   rule a    =>  b
diff --git a/test/all-path/02-constructors/00-case-analysis/path.k b/test/all-path/02-constructors/00-case-analysis/path.k
@@ -1,5 +1,5 @@
 module PATH
-  import BOOL
+  imports BOOL
   syntax S ::= "a" | "b" | "c"
   syntax T ::= total(S) | partial(S) | "end"
 
diff --git a/test/all-path/03-unification/set-select/path.k b/test/all-path/03-unification/set-select/path.k
@@ -1,7 +1,7 @@
 module PATH
-  import BOOL
-  import INT
-  import SET
+  imports BOOL
+  imports INT
+  imports SET
   syntax S ::= "a" | "b" | "c" 
   syntax Cmd ::= "select"
 
diff --git a/test/all-path/limitations/interfering-specs/path.k b/test/all-path/limitations/interfering-specs/path.k
@@ -1,5 +1,5 @@
 module PATH
-  import BOOL
+  imports BOOL
   syntax S ::= "a" | "b" | "c" | "d"
 
   rule a => b
diff --git a/test/functions/functions.k b/test/functions/functions.k
@@ -1,4 +1,4 @@
-require "harness.k"
+requires "harness.k"
 
 module FUNCTIONS
 
diff --git a/test/issue-1665/issue-1665-spec.k b/test/issue-1665/issue-1665-spec.k
@@ -1,7 +1,7 @@
 requires "test.k"
 
 module ISSUE-1665-SPEC
-  import TEST
+  imports TEST
 
   // Proving this claim requires inferring that the left-hand side of an
   // intermediate proof goal is defined.
diff --git a/test/issue-1665/test.k b/test/issue-1665/test.k
@@ -1,5 +1,5 @@
 module TEST-SYNTAX
-  import INT
+  imports INT
 
   syntax Pgm ::= "begin" Int | "end" Int
   syntax Int ::= fun(Int) [function, no-evaluators]
@@ -8,7 +8,7 @@ module TEST-SYNTAX
 endmodule
 
 module TEST
-  import TEST-SYNTAX
+  imports TEST-SYNTAX
 
   configuration <k> $PGM:Pgm </k>
 
diff --git a/test/issue-2138/issue-2138-spec.k b/test/issue-2138/issue-2138-spec.k
@@ -1,7 +1,7 @@
 requires "test.k"
 
 module ISSUE-2138-SPEC
-  import TEST
+  imports TEST
 
   claim
     <k> #assert i ( 1 , 0 ) ==Int 0 => . </k>
diff --git a/test/itp-nth-ancestor/chain.k b/test/itp-nth-ancestor/chain.k
@@ -3,7 +3,7 @@
     https://github.com/runtimeverification/casper-proofs/blob/master/Core/AccountableSafety.v
 */
 
-require "proof-script.k"
+requires "proof-script.k"
 
 module CHAIN-SYNTAX
 
diff --git a/test/itp-nth-ancestor/nth1-spec.k b/test/itp-nth-ancestor/nth1-spec.k
@@ -23,7 +23,7 @@
     by apply/connect1.
 */
 
-require "chain.k"
+requires "chain.k"
 
 // base case
 module NTH1-SPEC
diff --git a/test/itp-nth-ancestor/nth2-spec.k b/test/itp-nth-ancestor/nth2-spec.k
@@ -23,7 +23,7 @@
     by apply/connect1.
 */
 
-require "chain.k"
+requires "chain.k"
 
 // inductive case
 module NTH2-SPEC
diff --git a/test/k-equal/test-k-equal.k b/test/k-equal/test-k-equal.k
@@ -1,4 +1,4 @@
-require "domains.md"
+requires "domains.md"
 
 module TEST-K-EQUAL
     imports BOOL
diff --git a/test/lib/adomains.k b/test/lib/adomains.k
@@ -1,4 +1,4 @@
-require "domains.md"
+requires "domains.md"
 
 module ABOOL-SYNTAX
   syntax ABool ::= "Zero" | "One"
@@ -10,8 +10,8 @@ module AINT-SYNTAX
 endmodule
 
 module AINT
-  import AINT-SYNTAX
-  import ABOOL-SYNTAX
+  imports AINT-SYNTAX
+  imports ABOOL-SYNTAX
 
   syntax AInt
     ::= AInt "+AInt" AInt [function]
diff --git a/test/lib/astate.k b/test/lib/astate.k
@@ -1,5 +1,5 @@
-require "adomains.k"
-require "state.k"
+requires "adomains.k"
+requires "state.k"
 
 module ASTATE
   imports STATE-BASIC
diff --git a/test/overloads/simple-lists/simple-lists.k b/test/overloads/simple-lists/simple-lists.k
@@ -1,5 +1,5 @@
 module SIMPLE-LISTS
-    import BOOL
+    imports BOOL
     syntax EmptyStmt
  // ----------------
 
diff --git a/test/save-proofs/test-2-spec.k b/test/save-proofs/test-2-spec.k
@@ -1,7 +1,7 @@
 // Two claims, the first one should fail, but is loaded from the saved claims
 // for first.k, which allows the entire spec to pass.
 
-require "save-proofs.k"
+requires "save-proofs.k"
 
 module TEST-2-SPEC
   imports SAVE-PROOFS

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-require "harness.k"`
	`1`	`+requires "harness.k"`
`2`	`2`
`3`	`3`	`module FUNCTIONS`
`4`	`4`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-require "domains.md"`
	`1`	`+requires "domains.md"`
`2`	`2`
`3`	`3`	`module TEST-K-EQUAL`
`4`	`4`	`imports BOOL`