diff --git a/auxil.md b/auxil.md index a91d31c6d..1ed01b680 100644 --- a/auxil.md +++ b/auxil.md @@ -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 diff --git a/data/int-type.k b/data/int-type.k index 43bd31ab6..788695e39 100644 --- a/data/int-type.k +++ b/data/int-type.k @@ -1,6 +1,6 @@ module INT-TYPE - import INT + imports INT syntax WrappedInt syntax Int diff --git a/data/list-int.k b/data/list-int.k index f0040f8b5..f1f08d136 100644 --- a/data/list-int.k +++ b/data/list-int.k @@ -1,4 +1,4 @@ -require "int-type.k" +requires "int-type.k" module LIST-INT imports private INT-SYNTAX diff --git a/data/list-ref.k b/data/list-ref.k index deca3b299..4c2f437db 100644 --- a/data/list-ref.k +++ b/data/list-ref.k @@ -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 diff --git a/data/map-int-to-int.k b/data/map-int-to-int.k index 750d52724..6238a8e07 100644 --- a/data/map-int-to-int.k +++ b/data/map-int-to-int.k @@ -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 @@ -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] diff --git a/data/sparse-bytes.k b/data/sparse-bytes.k index 76125ac82..8fd5042a9 100644 --- a/data/sparse-bytes.k +++ b/data/sparse-bytes.k @@ -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)] diff --git a/data/tools.k b/data/tools.k index 5def535b7..90369b073 100644 --- a/data/tools.k +++ b/data/tools.k @@ -1,4 +1,4 @@ -require "list-int.k" +requires "list-int.k" module WASM-DATA-TOOLS imports BOOL diff --git a/numeric.md b/numeric.md index 7ca535992..730452a57 100644 --- a/numeric.md +++ b/numeric.md @@ -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 diff --git a/package/version b/package/version index 9faa1b7a7..c946ee616 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.5 +0.1.6 diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index 76c34f29b..29d5e334c 100644 --- a/pykwasm/pyproject.toml +++ b/pykwasm/pyproject.toml @@ -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. ", diff --git a/test.md b/test.md index 22ab590a6..4ecab4aa3 100644 --- a/test.md +++ b/test.md @@ -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. diff --git a/wasm-text.md b/wasm-text.md index 8246ba752..4bc30dec2 100644 --- a/wasm-text.md +++ b/wasm-text.md @@ -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 diff --git a/wasm.md b/wasm.md index 070405484..0353bc738 100644 --- a/wasm.md +++ b/wasm.md @@ -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