Merge pull request #1504 from cryspen/rengine-rust-engine-reflection-ocaml-reviewable

Rust Engine: transport the Rust AST to OCaml

Author: W95Psp

Cargo.lock

@@ -81,6 +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" }
 
 [workspace.metadata.release]
 owners = ["github:cryspen:tools"]

Cargo.toml

@@ -48,14 +48,21 @@ extension-traits = "1.0.1"
 serde.workspace = true
 serde_json.workspace = true
 hax-types.workspace = true
+rust-printer.workspace = true
 schemars.workspace = true
 hax-frontend-exporter.workspace = true
-hax-lib-macros-types = {workspace = true, features = ["schemars"]}
+hax-lib-macros-types = { workspace = true, features = ["schemars"] }
 version_check = "0.9"
 toml = "0.8"
 
 [package.metadata.release]
-pre-release-hook = ["dune", "build", "--root", "../../engine", "hax-engine.opam"]
+pre-release-hook = [
+    "dune",
+    "build",
+    "--root",
+    "../../engine",
+    "hax-engine.opam",
+]
 
 [[package.metadata.release.pre-release-replacements]]
 file = "../../engine/dune-project"

cli/subcommands/Cargo.toml

@@ -24,6 +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,
     ));
     schema.schema.metadata.get_or_insert_default().id = Some(hax_types::HAX_VERSION.into());
     serde_json::to_writer(

cli/subcommands/build.rs

@@ -0,0 +1,23 @@
+(** This module re-exports and renames a subset of `Types`.
+    `Types` contains both the modules from the frontend and from the Rust engine.
+    Thus, some types are deduplicated, and get renamed.
+*)
+
+module Renamed = struct
+  type arm = Types.arm2
+  type attribute = Types.attribute2
+  type attribute_kind = Types.attribute_kind2
+  type binding_mode = Types.binding_mode2
+  type borrow_kind = Types.borrow_kind2
+  type def_id = Types.def_id2
+  type expr_kind = Types.expr_kind2
+  type impl_expr = Types.impl_expr2
+  type param = Types.param2
+  type pat_kind = Types.pat_kind2
+  type projection_predicate = Types.projection_predicate2
+  type region = Types.region2
+  type span = Types.span2
+end
+
+include Types
+include Renamed

engine/lib/rust_engine_types.ml

@@ -438,7 +438,7 @@ let exporters = {
         },
     },
     empty_struct: {
-        guard: def => (eq(keys(def), new Set(["type"])) && def.type == 'object'),
+        guard: def => (eq(keys(def), new Set(["type"])) && (def.type == 'object' || def.type == 'null')),
         f: (name, _) => {
             return {
                 type: `EmptyStruct${name}`,
@@ -447,6 +447,21 @@ let exporters = {
             };
         },
     },
+    newtype: {
+        guard: def => !exporters['empty_struct'].guard(def) && is_type.expr(def, ["try-parse"]),
+        f: (name, o) => {
+            let path = [name + '-newtype-ref'];
+            let te = is_type.expr(o, path);
+            let ocaml_type = ocaml_of_type_expr(te, path);
+            let arms = ocaml_arms_of_type_expr(te, path);
+            let to_json = ocaml_yojson_of_type_expr(te, `(let Newtype${name} inner = o in inner)`, path);
+            return {
+                type: `Newtype${name} of ${ocaml_type}`,
+                parse: `Newtype${name}(${mk_match('o', arms, path)})`,
+                to_json,
+            };
+        },
+    },
     // object is a *flat* record
     object: {
         guard: def => (eq(keys(def), new Set(["type", "required", "properties"]))

engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js

@@ -12,3 +12,4 @@ readme.workspace = true
 hax-frontend-exporter = { path = "../frontend/exporter", default-features = false }
 serde = { workspace = true, features = ["derive"] }
 hax-rust-engine-macros = { path = "macros" }
+schemars.workspace = true

rust-printer/Cargo.toml

@@ -52,7 +52,10 @@ pub fn derive_group_for_ast(_attr: TokenStream, item: TokenStream) -> TokenStrea
 /// Derive the necessary [de]serialization related traits for nodes in the AST.
 #[proc_macro_attribute]
 pub fn derive_group_for_ast_serialization(_attr: TokenStream, item: TokenStream) -> TokenStream {
-    add_derive(item, quote! {::serde::Deserialize, ::serde::Serialize})
+    add_derive(
+        item,
+        quote! {::serde::Deserialize, ::serde::Serialize, ::schemars::JsonSchema},
+    )
 }
 
 /// Derive the basic necessary traits for nodes in the AST.