Skip to content

Commit

Permalink
Replace usages of priorities, require, and import (#582)
Browse files Browse the repository at this point in the history
* Replace deprecated tokens

* Set Version: 0.1.6

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
Scott-Guest and devops authored Feb 22, 2024
1 parent f65bbdc commit 989a738
Show file tree
Hide file tree
Showing 13 changed files with 26 additions and 26 deletions.
2 changes: 1 addition & 1 deletion auxil.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Auxiliary Wasm Commands
Generally useful commands that are not part of the actual Wasm semantics.

```k
require "wasm.md"
requires "wasm.md"
module WASM-AUXIL-SYNTAX
imports WASM-SYNTAX
Expand Down
2 changes: 1 addition & 1 deletion data/int-type.k
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

module INT-TYPE
import INT
imports INT

syntax WrappedInt
syntax Int
Expand Down
2 changes: 1 addition & 1 deletion data/list-int.k
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
require "int-type.k"
requires "int-type.k"

module LIST-INT
imports private INT-SYNTAX
Expand Down
2 changes: 1 addition & 1 deletion data/list-ref.k
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@


module LIST-REF
import WASM-DATA-INTERNAL-SYNTAX
imports WASM-DATA-INTERNAL-SYNTAX
imports private INT-SYNTAX
imports private BASIC-K

Expand Down
8 changes: 4 additions & 4 deletions data/map-int-to-int.k
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

require "int-type.k"
// require "int-type.k"
require "list-int.k"
requires "int-type.k"
// requires "int-type.k"
requires "list-int.k"

module MAP-INT-TO-INT
imports private BOOL-SYNTAX
Expand Down Expand Up @@ -33,7 +33,7 @@ module MAP-INT-TO-INT
injective
]

syntax priorities _Int2Int|->_ > _MapIntToInt_ .MapIntToInt
syntax priority _Int2Int|->_ > _MapIntToInt_ .MapIntToInt
syntax non-assoc _Int2Int|->_
syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]"
[function, hook(MAP.lookup), klabel(MapIntToInt:lookup), symbol]
Expand Down
6 changes: 3 additions & 3 deletions data/sparse-bytes.k
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@

module SPARSE-BYTES
import BOOL
import BYTES
import INT
imports BOOL
imports BYTES
imports INT

syntax SBItem ::= #empty(Int) [symbol, klabel(SBItem:empty)]
| #bytes(Bytes) [symbol, klabel(SBItem:bytes)]
Expand Down
2 changes: 1 addition & 1 deletion data/tools.k
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
require "list-int.k"
requires "list-int.k"

module WASM-DATA-TOOLS
imports BOOL
Expand Down
2 changes: 1 addition & 1 deletion numeric.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ In this file we implement the numeric rules specified in section `4.3 Numerics`
In the notations of some operators, `sx` is the signedness of the operator and could be either `s` (signed) or `u` (unsigned), which indicates whether the operands should be interpreted as signed integer or unsigned integer.

```k
require "data.md"
requires "data.md"
module WASM-NUMERIC-SYNTAX
Expand Down
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.5
0.1.6
2 changes: 1 addition & 1 deletion pykwasm/pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pykwasm"
version = "0.1.5"
version = "0.1.6"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
4 changes: 2 additions & 2 deletions test.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@ KWasm Testing
For testing, we augment the semantics with some helpers.

```k
require "wasm-text.md"
require "auxil.md"
requires "wasm-text.md"
requires "auxil.md"
```

Module `WASM-TEST-SYNTAX` is just used for program parsing and `WASM-TEST` consists of the definitions both for parsing and execution.
Expand Down
4 changes: 2 additions & 2 deletions wasm-text.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ WebAssembly Text Format
=======================

```k
require "wasm.md"
require "data.md"
requires "wasm.md"
requires "data.md"
module WASM-TEXT-SYNTAX
imports WASM-SYNTAX
Expand Down
14 changes: 7 additions & 7 deletions wasm.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@ WebAssembly State and Semantics
===============================

```k
require "data.md"
require "data/list-int.k"
require "data/list-ref.k"
require "data/map-int-to-int.k"
require "data/sparse-bytes.k"
require "data/tools.k"
require "numeric.md"
requires "data.md"
requires "data/list-int.k"
requires "data/list-ref.k"
requires "data/map-int-to-int.k"
requires "data/sparse-bytes.k"
requires "data/tools.k"
requires "numeric.md"
module WASM-SYNTAX
imports WASM-DATA-SYNTAX
Expand Down

0 comments on commit 989a738

Please sign in to comment.