Merge pull request #1507 from cryspen/rengine-rename-rust-printer-to-rust-engine

Rust Engine: rename rust printer to rust engine

Author: W95Psp

.github/workflows/clippy_rust_engine.yml

@@ -15,4 +15,4 @@ jobs:
     - uses: actions/checkout@v4
     - name: Run clippy
       run: |
-        cargo clippy -p rust-printer -- --no-deps
+        cargo clippy -p hax-rust-engine -- --no-deps

Cargo.lock

@@ -14,10 +14,10 @@ members = [
      "engine/names",
      "engine/names/extract",
      "hax-types",
-     "rust-printer",
-     "rust-printer/macros",
+     "rust-engine",
+     "rust-engine/macros",
 ]
-exclude = ["tests", "rustc-coverage-tests", "rust-printer/tests"]
+exclude = ["tests", "rustc-coverage-tests", "rust-engine/tests"]
 default-members = [
      "frontend/exporter",
      "frontend/exporter/options",
@@ -81,7 +81,7 @@ hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.3.1" }
 hax-lib = { path = "hax-lib", version = "=0.3.1" }
 hax-engine-names = { path = "engine/names", version = "=0.3.1" }
 hax-types = { path = "hax-types", version = "=0.3.1" }
-rust-printer = { path = "rust-printer" }
+hax-rust-engine = { path = "rust-engine" }
 
 [workspace.metadata.release]
 owners = ["github:cryspen:tools"]

Cargo.toml

@@ -48,7 +48,7 @@ extension-traits = "1.0.1"
 serde.workspace = true
 serde_json.workspace = true
 hax-types.workspace = true
-rust-printer.workspace = true
+hax-rust-engine.workspace = true
 schemars.workspace = true
 hax-frontend-exporter.workspace = true
 hax-lib-macros-types = { workspace = true, features = ["schemars"] }

cli/subcommands/Cargo.toml

@@ -24,7 +24,7 @@ fn json_schema_static_asset() {
         hax_types::engine_api::protocol::FromEngine,
         hax_types::engine_api::protocol::ToEngine,
         hax_lib_macros_types::AttrPayload,
-        rust_printer::ast::Item,
+        hax_rust_engine::ast::Item,
     ));
     schema.schema.metadata.get_or_insert_default().id = Some(hax_types::HAX_VERSION.into());
     serde_json::to_writer(

cli/subcommands/build.rs

@@ -149,12 +149,12 @@ These tests aim at increasing the confidence in the ability of hax frontend to h
 
 ### Rust printer testing
 
-This method aims at testing the quality of hax frontend's output. It uses a tool that is under development that we call the Rust printer.
+This method aims at testing the quality of hax frontend's output. It uses the Rust hax engine.
 
 This tool (written in Rust) takes the output of hax frontend (a json file describing the content of a Rust crate), it imports it as an AST (similar to the hax engine AST), and then prints this AST in Rust syntax. 
 
 If the Rust code we get out of this tool is equivalent to the Rust code it was given as input, then this means hax frontend correctly extracted the input code without losing or altering any information.
 
 There is no easy way of testing the full input/output equivalence so the methodology here is to test that the resulting code behaves the same as the input code with respect to relevant test cases.
 
-This work is available in the `rust-printer` folder. In the `tests` subfolder, an input file is available with tests for all Rust constructs supported by the printer (currently functions and expressions). For now these tests pass after extracting and printing the file with hax frontend and the Rust printer. This means that for the Rust constructs covered by the printer and the test file, hax frontend's extraction is correct. However this still needs to be extended to test more Rust constructs.
+This work is available in the `hax-rust-engine` folder. In the `tests` subfolder, an input file is available with tests for all Rust constructs supported by the printer (currently functions and expressions). For now these tests pass after extracting and printing the file with hax frontend and the Rust printer. This means that for the Rust constructs covered by the printer and the test file, hax frontend's extraction is correct. However this still needs to be extended to test more Rust constructs.

docs/frontend/evaluation.md

@@ -1,5 +1,5 @@
 [package]
-name = "rust-printer"
+name = "hax-rust-engine"
 version.workspace = true
 authors.workspace = true
 license.workspace = true

rust-printer/Cargo.toml renamed to rust-engine/Cargo.toml

@@ -6,9 +6,9 @@ This crate should implement an AST for which:
  5. This AST should be suitable for AST transformations.
 
 ## Usage
-`rust-printer` expects it's stdin to be the output of `cargo hax json`, e.g.:
+`hax-rust-engine` expects it's stdin to be the output of `cargo hax json`, e.g.:
 ```bash
-cargo hax json -o - | rust-printer > output.rs
+cargo hax json -o - | hax-rust-engine > output.rs
 ```
 
 ## Test