From eef5801f3d0fd27deb624e407971ed4afde71b20 Mon Sep 17 00:00:00 2001 From: Virgil Date: Mon, 26 Aug 2024 15:49:32 +0300 Subject: [PATCH 1/2] Import only the configuration parts that are strictly needed. --- rust-semantics/execution/calls.md | 10 ++++++---- rust-semantics/execution/stack.md | 5 +++-- rust-semantics/preprocessing/constants.md | 3 ++- rust-semantics/preprocessing/crate.md | 2 +- rust-semantics/preprocessing/initialization.md | 3 ++- rust-semantics/rust-common.md | 1 - rust-semantics/targets/execution/configuration.md | 13 ++++++++++--- rust-semantics/targets/execution/rust.md | 1 + .../targets/preprocessing/configuration.md | 12 ++++++++++-- rust-semantics/targets/preprocessing/rust.md | 3 ++- rust-semantics/test/execution.md | 13 ++++++++----- 11 files changed, 45 insertions(+), 21 deletions(-) diff --git a/rust-semantics/execution/calls.md b/rust-semantics/execution/calls.md index a106844..7ea8177 100644 --- a/rust-semantics/execution/calls.md +++ b/rust-semantics/execution/calls.md @@ -2,10 +2,12 @@ module RUST-CALLS imports BOOL - imports RUST-STACK - imports RUST-HELPERS - imports RUST-REPRESENTATION - imports RUST-RUNNING-CONFIGURATION + imports private COMMON-K-CELL + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-HELPERS + imports private RUST-PREPROCESSING-CONFIGURATION + imports private RUST-REPRESENTATION + imports private RUST-STACK // https://doc.rust-lang.org/stable/reference/expressions/method-call-expr.html diff --git a/rust-semantics/execution/stack.md b/rust-semantics/execution/stack.md index 8652a1f..c01475f 100644 --- a/rust-semantics/execution/stack.md +++ b/rust-semantics/execution/stack.md @@ -1,8 +1,9 @@ ```k module RUST-STACK - imports LIST - imports RUST-RUNNING-CONFIGURATION + imports private COMMON-K-CELL + imports private LIST + imports private RUST-EXECUTION-CONFIGURATION syntax Instruction ::= "pushLocalState" | "popLocalState" diff --git a/rust-semantics/preprocessing/constants.md b/rust-semantics/preprocessing/constants.md index 43fbcd7..db7a118 100644 --- a/rust-semantics/preprocessing/constants.md +++ b/rust-semantics/preprocessing/constants.md @@ -1,8 +1,9 @@ ```k module RUST-CONSTANTS + imports private COMMON-K-CELL imports private RUST-CASTS + imports private RUST-PREPROCESSING-CONFIGURATION imports private RUST-REPRESENTATION - imports private RUST-RUNNING-CONFIGURATION imports private RUST-SHARED-SYNTAX syntax KItem ::= setConstant(Identifier, ValueOrError) diff --git a/rust-semantics/preprocessing/crate.md b/rust-semantics/preprocessing/crate.md index a305429..66d5e3b 100644 --- a/rust-semantics/preprocessing/crate.md +++ b/rust-semantics/preprocessing/crate.md @@ -1,12 +1,12 @@ ```k module CRATE + imports private COMMON-K-CELL imports private LIST imports private MAP imports private RUST-PREPROCESSING-PRIVATE-SYNTAX imports private RUST-PREPROCESSING-SYNTAX imports private RUST-REPRESENTATION - imports private RUST-RUNNING-CONFIGURATION syntax Initializer ::= crateParser(crate: Crate, traitName: MaybeIdentifier, traitFunctions: Map) diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md index e35e93d..2e4ff58 100644 --- a/rust-semantics/preprocessing/initialization.md +++ b/rust-semantics/preprocessing/initialization.md @@ -1,7 +1,8 @@ ```k module INITIALIZATION - imports private RUST-RUNNING-CONFIGURATION + imports private COMMON-K-CELL + imports private RUST-PREPROCESSING-CONFIGURATION imports private RUST-PREPROCESSING-PRIVATE-HELPERS imports private RUST-PREPROCESSING-PRIVATE-SYNTAX diff --git a/rust-semantics/rust-common.md b/rust-semantics/rust-common.md index 41c1abc..ecacecc 100644 --- a/rust-semantics/rust-common.md +++ b/rust-semantics/rust-common.md @@ -13,7 +13,6 @@ module RUST-COMMON imports RUST-HELPERS imports RUST-PREPROCESSING imports RUST-REPRESENTATION - imports RUST-RUNNING-CONFIGURATION imports RUST-SHARED-SYNTAX endmodule diff --git a/rust-semantics/targets/execution/configuration.md b/rust-semantics/targets/execution/configuration.md index 27781ab..e5f0d55 100644 --- a/rust-semantics/targets/execution/configuration.md +++ b/rust-semantics/targets/execution/configuration.md @@ -1,14 +1,21 @@ ```k -module RUST-RUNNING-CONFIGURATION - imports private RUST-PREPROCESSING-SYNTAX +module COMMON-K-CELL imports private RUST-EXECUTION-TEST-PARSING-SYNTAX + imports private RUST-PREPROCESSING-SYNTAX + + configuration + crateParser($PGM:Crate) ~> $TEST:ExecutionTest +endmodule + +module RUST-RUNNING-CONFIGURATION + imports COMMON-K-CELL imports RUST-CONFIGURATION imports RUST-EXECUTION-TEST-CONFIGURATION configuration - crateParser($PGM:Crate) ~> $TEST:ExecutionTest + diff --git a/rust-semantics/targets/execution/rust.md b/rust-semantics/targets/execution/rust.md index d6a0c33..d051f5f 100644 --- a/rust-semantics/targets/execution/rust.md +++ b/rust-semantics/targets/execution/rust.md @@ -13,6 +13,7 @@ endmodule module RUST imports RUST-COMMON imports RUST-EXECUTION-TEST + imports RUST-RUNNING-CONFIGURATION endmodule ``` \ No newline at end of file diff --git a/rust-semantics/targets/preprocessing/configuration.md b/rust-semantics/targets/preprocessing/configuration.md index 9238cbf..7b41f3e 100644 --- a/rust-semantics/targets/preprocessing/configuration.md +++ b/rust-semantics/targets/preprocessing/configuration.md @@ -1,12 +1,20 @@ ```k -module RUST-RUNNING-CONFIGURATION +module COMMON-K-CELL imports private RUST-PREPROCESSING-SYNTAX + + configuration + crateParser($PGM:Crate) + +endmodule + +module RUST-RUNNING-CONFIGURATION + imports COMMON-K-CELL imports RUST-CONFIGURATION configuration - crateParser($PGM:Crate) + endmodule diff --git a/rust-semantics/targets/preprocessing/rust.md b/rust-semantics/targets/preprocessing/rust.md index ca5122a..74ee243 100644 --- a/rust-semantics/targets/preprocessing/rust.md +++ b/rust-semantics/targets/preprocessing/rust.md @@ -9,7 +9,8 @@ module RUST-SYNTAX endmodule module RUST - imports RUST-COMMON + imports private RUST-RUNNING-CONFIGURATION + imports private RUST-COMMON endmodule ``` diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md index 77e6021..7d92941 100644 --- a/rust-semantics/test/execution.md +++ b/rust-semantics/test/execution.md @@ -10,11 +10,14 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX endmodule module RUST-EXECUTION-TEST - imports LIST - imports RUST-EXECUTION-TEST-PARSING-SYNTAX - imports RUST-HELPERS - imports RUST-REPRESENTATION - imports RUST-RUNNING-CONFIGURATION + imports private COMMON-K-CELL + imports private LIST + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-EXECUTION-TEST-PARSING-SYNTAX + imports private RUST-EXECUTION-TEST-CONFIGURATION + imports private RUST-HELPERS + imports private RUST-PREPROCESSING-CONFIGURATION + imports private RUST-REPRESENTATION rule E:ExecutionItem ; Es:ExecutionTest => E ~> Es rule .ExecutionTest => .K From e2086913ece7e58526d9593c4ffdcb5465a1f56c Mon Sep 17 00:00:00 2001 From: Virgil Date: Mon, 26 Aug 2024 16:10:06 +0300 Subject: [PATCH 2/2] Filter preprocessing imports --- rust-semantics/targets/preprocessing/configuration.md | 6 ++++-- rust-semantics/targets/preprocessing/rust.md | 7 +++++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/rust-semantics/targets/preprocessing/configuration.md b/rust-semantics/targets/preprocessing/configuration.md index 7b41f3e..d122260 100644 --- a/rust-semantics/targets/preprocessing/configuration.md +++ b/rust-semantics/targets/preprocessing/configuration.md @@ -10,12 +10,14 @@ endmodule module RUST-RUNNING-CONFIGURATION imports COMMON-K-CELL - imports RUST-CONFIGURATION + imports RUST-PREPROCESSING-CONFIGURATION configuration - + + + endmodule diff --git a/rust-semantics/targets/preprocessing/rust.md b/rust-semantics/targets/preprocessing/rust.md index 74ee243..0390e57 100644 --- a/rust-semantics/targets/preprocessing/rust.md +++ b/rust-semantics/targets/preprocessing/rust.md @@ -1,7 +1,9 @@ ```k requires "configuration.md" -requires "../../rust-common.md" +requires "../../preprocessing.md" +requires "../../representation.md" +requires "../../expression.md" requires "../../rust-common-syntax.md" module RUST-SYNTAX @@ -9,8 +11,9 @@ module RUST-SYNTAX endmodule module RUST + imports private RUST-EXPRESSION + imports private RUST-PREPROCESSING imports private RUST-RUNNING-CONFIGURATION - imports private RUST-COMMON endmodule ```