Skip to content

Commit

Permalink
Refactor kompilation targets. (#86)
Browse files Browse the repository at this point in the history
I'm planning to add multiple testing targets for mx-rust that differ only in the initial contents of the K cell (the better way of doing this would be to run tests with a pyk-based script, but that's more work).
  • Loading branch information
virgil-serbanuta authored Sep 16, 2024
1 parent 2571d71 commit 50d04af
Show file tree
Hide file tree
Showing 8 changed files with 84 additions and 88 deletions.
14 changes: 4 additions & 10 deletions mx-rust-semantics/targets/blockchain/mx-rust.md
Original file line number Diff line number Diff line change
@@ -1,21 +1,15 @@
```k
requires "configuration.md"
requires "mx-semantics/main/mx-common.md"
requires "mx-semantics/main/syntax.md"
requires "rust-semantics/rust-common.md"
requires "rust-semantics/rust-common-syntax.md"
requires "../../main/mx-rust-common.md"
requires "../common/mx-rust.md"
module MX-RUST-SYNTAX
imports RUST-COMMON-SYNTAX
imports MX-RUST-COMMON-TARGET-SYNTAX
endmodule
module MX-RUST
imports private MX-COMMON
imports private MX-RUST-COMMON
imports private MX-RUST-CONFIGURATION
imports private RUST-COMMON
imports private COMMON-K-CELL
imports private MX-RUST-COMMON-TARGET
endmodule
```
19 changes: 19 additions & 0 deletions mx-rust-semantics/targets/common/configuration-testing.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
```k
requires "../../main/configuration.md"
requires "../../test/configuration.md"
module MX-RUST-CONFIGURATION
imports COMMON-K-CELL
imports MX-RUST-COMMON-CONFIGURATION
imports MX-RUST-EXECUTION-TEST-CONFIGURATION
configuration
<mx-rust-cfg>
<mx-rust-test/>
<mx-rust/>
<k/>
</mx-rust-cfg>
endmodule
```
33 changes: 33 additions & 0 deletions mx-rust-semantics/targets/common/mx-rust-testing.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
```k
requires "configuration-testing.md"
requires "mx-rust.md"
requires "mx-semantics/main/mx-common.md"
requires "mx-semantics/main/syntax.md"
requires "mx-semantics/setup/setup.md"
requires "mx-semantics/test/configuration.md"
requires "mx-semantics/test/execution.md"
requires "rust-semantics/rust-common.md"
requires "rust-semantics/rust-common-syntax.md"
requires "rust-semantics/test/configuration.md"
requires "rust-semantics/test/execution.md"
requires "../../main/mx-rust-common.md"
requires "../../main/representation.md"
requires "../../setup/mx.md"
requires "../../test/execution.md"
module MX-RUST-COMMON-TEST-SYNTAX
imports RUST-COMMON-SYNTAX
imports MX-RUST-TESTING-PARSING-SYNTAX
endmodule
module MX-RUST-COMMON-TEST
imports private MX-RUST-COMMON-TARGET
imports private MX-RUST-TEST
imports private MX-RUST-SETUP-MX
imports private MX-SETUP
imports private MX-TEST-EXECUTION
imports private RUST-EXECUTION-TEST
endmodule
```
20 changes: 20 additions & 0 deletions mx-rust-semantics/targets/common/mx-rust.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
```k
requires "mx-semantics/main/mx-common.md"
requires "mx-semantics/main/syntax.md"
requires "rust-semantics/rust-common.md"
requires "rust-semantics/rust-common-syntax.md"
requires "../../main/mx-rust-common.md"
module MX-RUST-COMMON-TARGET-SYNTAX
imports RUST-COMMON-SYNTAX
endmodule
module MX-RUST-COMMON-TARGET
imports private MX-COMMON
imports private MX-RUST-COMMON
imports private MX-RUST-CONFIGURATION
imports private RUST-COMMON
endmodule
```
16 changes: 0 additions & 16 deletions mx-rust-semantics/targets/contract-testing/configuration.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
```k
requires "../../main/configuration.md"
requires "../../test/configuration.md"
module COMMON-K-CELL
imports MX-RUST-REPRESENTATION
imports RUST-SHARED-SYNTAX
Expand All @@ -23,17 +20,4 @@ module COMMON-K-CELL
</k>
endmodule
module MX-RUST-CONFIGURATION
imports COMMON-K-CELL
imports MX-RUST-COMMON-CONFIGURATION
imports MX-RUST-EXECUTION-TEST-CONFIGURATION
configuration
<mx-rust-cfg>
<mx-rust-test/>
<mx-rust/>
<k/>
</mx-rust-cfg>
endmodule
```
28 changes: 4 additions & 24 deletions mx-rust-semantics/targets/contract-testing/mx-rust.md
Original file line number Diff line number Diff line change
@@ -1,35 +1,15 @@
```k
requires "configuration.md"
requires "mx-semantics/main/mx-common.md"
requires "mx-semantics/main/syntax.md"
requires "mx-semantics/setup/setup.md"
requires "mx-semantics/test/configuration.md"
requires "mx-semantics/test/execution.md"
requires "rust-semantics/rust-common.md"
requires "rust-semantics/rust-common-syntax.md"
requires "rust-semantics/test/configuration.md"
requires "rust-semantics/test/execution.md"
requires "../../main/mx-rust-common.md"
requires "../../main/representation.md"
requires "../../setup/mx.md"
requires "../../test/execution.md"
requires "../common/mx-rust-testing.md"
module MX-RUST-SYNTAX
imports RUST-COMMON-SYNTAX
imports MX-RUST-TESTING-PARSING-SYNTAX
imports MX-RUST-COMMON-TEST-SYNTAX
endmodule
module MX-RUST
imports private MX-COMMON
imports private MX-RUST-TEST
imports private MX-RUST-CONFIGURATION
imports private MX-RUST-COMMON
imports private MX-RUST-SETUP-MX
imports private MX-SETUP
imports private MX-TEST-EXECUTION
imports private RUST-COMMON
imports private RUST-EXECUTION-TEST
imports private COMMON-K-CELL
imports private MX-RUST-COMMON-TEST
endmodule
```
16 changes: 0 additions & 16 deletions mx-rust-semantics/targets/testing/configuration.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
```k
requires "../../main/configuration.md"
requires "../../test/configuration.md"
module COMMON-K-CELL
imports MX-RUST-REPRESENTATION
imports RUST-PREPROCESSING-SYNTAX
Expand All @@ -14,17 +11,4 @@ module COMMON-K-CELL
<k> crateParser($PGM:Crate) ~> mxRustPreprocessTraits ~> ($TEST:MxRustTest):KItem </k>
endmodule
module MX-RUST-CONFIGURATION
imports COMMON-K-CELL
imports MX-RUST-COMMON-CONFIGURATION
imports MX-RUST-EXECUTION-TEST-CONFIGURATION
configuration
<mx-rust-cfg>
<mx-rust-test/>
<mx-rust/>
<k/>
</mx-rust-cfg>
endmodule
```
26 changes: 4 additions & 22 deletions mx-rust-semantics/targets/testing/mx-rust.md
Original file line number Diff line number Diff line change
@@ -1,33 +1,15 @@
```k
requires "configuration.md"
requires "mx-semantics/main/mx-common.md"
requires "mx-semantics/main/syntax.md"
requires "mx-semantics/setup/setup.md"
requires "mx-semantics/test/configuration.md"
requires "mx-semantics/test/execution.md"
requires "rust-semantics/rust-common.md"
requires "rust-semantics/rust-common-syntax.md"
requires "rust-semantics/test/configuration.md"
requires "rust-semantics/test/execution.md"
requires "../../main/mx-rust-common.md"
requires "../../main/representation.md"
requires "../../test/execution.md"
requires "../common/mx-rust-testing.md"
module MX-RUST-SYNTAX
imports RUST-COMMON-SYNTAX
imports MX-RUST-TESTING-PARSING-SYNTAX
imports MX-RUST-COMMON-TEST-SYNTAX
endmodule
module MX-RUST
imports private MX-COMMON
imports private MX-SETUP
imports private MX-RUST-TEST
imports private MX-RUST-CONFIGURATION
imports private MX-RUST-COMMON
imports private MX-TEST-EXECUTION
imports private RUST-COMMON
imports private RUST-EXECUTION-TEST
imports private COMMON-K-CELL
imports private MX-RUST-COMMON-TEST
endmodule
```

0 comments on commit 50d04af

Please sign in to comment.