Rengine bridge from rust rebased

cli/subcommands/src/cargo_hax.rs

@@ -298,7 +298,7 @@ fn run_engine(
     let mut output = Output {
         diagnostics: vec![],
         files: vec![],
-        debug_json: None,
+        debug_json: vec![],
     };
     {
         let mut rctx = hax_types::diagnostics::report::ReportCtx::default();
@@ -396,9 +396,7 @@ fn run_engine(
                         HaxMessage::ProducedFile { path, wrote }.report(message_format, None)
                     }
                 }
-                FromEngine::DebugString(debug) => {
-                    output.debug_json = Some(debug);
-                }
+                FromEngine::DebugString(debug) => output.debug_json.push(debug),
                 FromEngine::PrettyPrintDiagnostic(diag) => {
                     send!(&ToEngine::PrettyPrintedDiagnostic(format!("{}", diag)));
                 }
@@ -447,8 +445,9 @@ fn run_engine(
     if backend.dry_run {
         serde_json::to_writer(std::io::BufWriter::new(std::io::stdout()), &output).unwrap()
     }
-    if let Some(debug_json) = &output.debug_json {
+    if !output.debug_json.is_empty() {
         use DebugEngineMode;
+        let debug_json = &format!("[{}]", output.debug_json.join(","));
         match &backend.debug_engine {
             Some(DebugEngineMode::Interactive) => {
                 eprintln!("----------------------------------------------");

engine/bin/lib.ml

@@ -157,7 +157,7 @@ let run (options : Types.engine_options) : Types.output =
   {
     diagnostics = List.map ~f:Diagnostics.to_thir_diagnostic diagnostics;
     files = Option.value ~default:[] files;
-    debug_json = None;
+    debug_json = [];
   }
 
 (** Shallow parses a `id_table::Node<T>` (or a raw `T`) JSON *)
@@ -224,6 +224,10 @@ let parse_options () =
   Profiling.enabled := options.backend.profile;
   options
 
+let send_debug_strings =
+  Phase_utils.DebugBindPhase.export
+  >> List.iter ~f:(fun json -> DebugString json |> Hax_io.write)
+
 (** Entrypoint of the engine. Assumes `Hax_io.init` was called. *)
 let engine () =
   let options = Profiling.profile (Other "parse_options") 1 parse_options in
@@ -241,26 +245,49 @@ let engine () =
   in
   match result with
   | Ok results ->
-      let debug_json = Phase_utils.DebugBindPhase.export () in
-      let results = { results with debug_json } in
-      Logs.info (fun m -> m "Outputting JSON");
-
       List.iter
         ~f:(fun diag -> Diagnostic diag |> Hax_io.write)
         results.diagnostics;
       List.iter ~f:(fun file -> File file |> Hax_io.write) results.files;
 
-      Option.iter ~f:(fun json -> DebugString json |> Hax_io.write) debug_json;
+      send_debug_strings ();
       Hax_io.close ();
 
       Logs.info (fun m -> m "Exiting Hax engine (success)")
   | Error (exn, bt) ->
       Logs.info (fun m -> m "Exiting Hax engine (with an unexpected failure)");
       Printexc.raise_with_backtrace exn bt
 
+module ExportFullAst = Export_ast.Make (Features.Full)
 module ExportRustAst = Export_ast.Make (Features.Rust)
 module ExportLeanAst = Export_ast.Make (Lean_backend.InputLanguage)
 
+let driver_for_rust_engine_inner (query : Rust_engine_types.query) :
+    Rust_engine_types.response =
+  Profiling.enabled := query.profiling;
+  if query.debug_bind_phase then Phase_utils.DebugBindPhase.enable ();
+  match query.kind with
+  | Types.ImportThir { input; translation_options } ->
+      let imported_items =
+        import_thir_items translation_options.include_namespaces input
+      in
+      let rust_ast_items =
+        List.concat_map ~f:ExportRustAst.ditem imported_items
+      in
+      Rust_engine_types.ImportThir { output = rust_ast_items }
+  | Types.ApplyPhases { input; phases } ->
+      let items = List.concat_map ~f:Import_ast.ditem input in
+      let module Phase =
+        (val List.map
+               ~f:(fun name ->
+                 Untyped_phases.phase_of_name name |> Option.value_exn)
+               phases
+             |> Untyped_phases.bind_list)
+      in
+      let items = Phase.ditems items in
+      let output = List.concat_map ~f:ExportFullAst.ditem items in
+      Rust_engine_types.ApplyPhases { output }
+
 (** Entry point for interacting with the Rust hax engine *)
 let driver_for_rust_engine () : unit =
   let query : Rust_engine_types.query =
@@ -269,23 +296,7 @@ let driver_for_rust_engine () : unit =
   in
   Concrete_ident.ImplInfoStore.init
     (Concrete_ident_generated.impl_infos @ query.impl_infos);
-  match query.kind with
-  | Types.ImportThir { input; apply_phases; translation_options } ->
-      (* Note: `apply_phases` comes from the type `QueryKind` in
-       `ocaml_engine.rs`. This is a temporary flag that applies some phases while
-       importing THIR. In the future (when #1550 is merged), we will be able to
-       import THIR and then apply phases. *)
-      let imported_items =
-        import_thir_items translation_options.include_namespaces input
-      in
-      let rust_ast_items =
-        if apply_phases then
-          let imported_items = Lean_backend.apply_phases imported_items in
-          List.concat_map
-            ~f:(fun item -> ExportLeanAst.ditem item)
-            imported_items
-        else List.concat_map ~f:ExportRustAst.ditem imported_items
-      in
-      let response = Rust_engine_types.ImportThir { output = rust_ast_items } in
-      Hax_io.write_json ([%yojson_of: Rust_engine_types.response] response);
-      Hax_io.write_json ([%yojson_of: Types.from_engine] Exit)
+  let response = driver_for_rust_engine_inner query in
+  send_debug_strings ();
+  Hax_io.write_json ([%yojson_of: Rust_engine_types.response] response);
+  Hax_io.write_json ([%yojson_of: Types.from_engine] Exit)

engine/lib/ast_utils.ml

@@ -909,6 +909,67 @@ module Make (F : Features.T) = struct
   let string_lit span (s : string) : expr =
     { span; typ = TStr; e = Literal (String s) }
 
+  module HaxFailure = struct
+    module Build = struct
+      let pat span (typ : ty) (msg : string) : pat =
+        let (module M) = M.make span in
+        let constructor =
+          Global_ident.of_name ~value:true Rust_primitives__hax__Failure__Ctor
+        in
+        let pat = M.pat_PConstant ~typ ~lit:(String msg) in
+        let fields = [ { field = constructor; pat } ] in
+        M.pat_PConstruct ~typ ~is_record:false ~is_struct:true ~constructor
+          ~fields
+
+      let expr span (typ : ty) (error : string) (ast : string) =
+        let args = List.map ~f:(string_lit span) [ error; ast ] in
+        call Rust_primitives__hax__failure args span typ
+
+      let ty (payload : string) =
+        let ident =
+          `Concrete
+            (Concrete_ident.of_name ~value:false Rust_primitives__hax__Failure)
+        in
+        let (module M) = M.make (Span.dummy ()) in
+        let payload = M.expr_Literal ~typ:TBool (String payload) in
+        TApp { ident; args = [ GConst payload ] }
+    end
+
+    open struct
+      let destruct_str_lit e =
+        let* l = D.expr_Literal e in
+        match l with String s -> Some s | _ -> None
+    end
+
+    module Destruct = struct
+      let pat (p : pat) : string option =
+        let* p = D.pat_PConstruct p in
+        let*? () =
+          Global_ident.eq_name Rust_primitives__hax__Failure__Ctor p.constructor
+        in
+        let* { pat; _ } = D.list_1 p.fields in
+        let* s = D.pat_PConstant pat in
+        match s.lit with String s -> Some s | _ -> None
+
+      let expr (e : expr) : (string * string) option =
+        let* app = D.expr_App e in
+        let* id = D.expr_GlobalVar app.f in
+        let*? _ = Global_ident.eq_name Rust_primitives__hax__failure id in
+        let* x, y = D.list_2 app.args in
+
+        let* x = destruct_str_lit x in
+        let* y = destruct_str_lit y in
+        Some (x, y)
+
+      let ty (t : ty) : string option =
+        match t with
+        | TApp { ident; args = [ GConst payload ] }
+          when Global_ident.eq_name Rust_primitives__hax__Failure ident ->
+            destruct_str_lit payload
+        | _ -> None
+    end
+  end
+
   let hax_failure_expr' span (typ : ty) (context, kind) (ast : string) =
     let ast =
       (* Remove consecutive withe spaces *)
@@ -921,19 +982,11 @@ module Make (F : Features.T) = struct
       else ast
     in
     let error = Diagnostics.pretty_print_context_kind context kind in
-    let args = List.map ~f:(string_lit span) [ error; ast ] in
-    call Rust_primitives__hax__failure args span typ
+    HaxFailure.Build.expr span typ error ast
 
   let hax_failure_expr span (typ : ty) (context, kind) (expr0 : Ast.Full.expr) =
     hax_failure_expr' span typ (context, kind) (Print_rust.pexpr_str expr0)
 
-  let hax_failure_typ =
-    let ident =
-      `Concrete
-        (Concrete_ident.of_name ~value:false Rust_primitives__hax__failure)
-    in
-    TApp { ident; args = [] }
-
   module LiftToFullAst = struct
     let expr : AST.expr -> Ast.Full.expr = Stdlib.Obj.magic
     let ty : AST.ty -> Ast.Full.ty = Stdlib.Obj.magic

engine/lib/concrete_ident/explicit_def_id.ml

@@ -149,7 +149,7 @@ module FromRustAST = struct
       ({ krate; path; parent; kind; _ } : A.def_id) : B.def_id_contents =
     let f (o : A.def_id) : B.def_id =
       let contents : B.node_for__def_id_contents =
-        { value = def_id_contents_to_rust_ast o; id = Int64.of_int (-1) }
+        { value = def_id_contents_to_rust_ast o; id = Int64.zero }
       in
       { contents }
     in
@@ -159,13 +159,15 @@ module FromRustAST = struct
       path;
       parent;
       kind;
-      index = (Int64.of_int (-1), Int64.of_int (-1), None);
+      index = (Int64.zero, Int64.zero, None);
       is_local = false;
     }
 
   let to_rust_ast ({ is_constructor; def_id } : A.explicit_def_id) : t =
     { is_constructor; def_id = def_id_contents_to_rust_ast def_id }
 end
 
+let def_id_to_rust_ast = ToRustAST.def_id_contents_to_rust_ast
+let def_id_from_rust_ast = FromRustAST.def_id_contents_to_rust_ast
 let to_rust_ast = ToRustAST.to_rust_ast
 let from_rust_ast = FromRustAST.to_rust_ast

engine/lib/concrete_ident/explicit_def_id.mli

@@ -84,5 +84,7 @@ module ImplInfoStore : sig
       [None] even though the supplied identifier points to an [Impl] block. *)
 end
 
+val def_id_to_rust_ast : Types.def_id_contents -> Types.def_id_inner
+val def_id_from_rust_ast : Types.def_id_inner -> Types.def_id_contents
 val to_rust_ast : t -> Rust_engine_types.explicit_def_id
 val from_rust_ast : Rust_engine_types.explicit_def_id -> t

engine/lib/diagnostics.ml

@@ -10,6 +10,7 @@ module Phase = struct
   module Rejection = struct
     type t =
       | NotInBackendLang of Backend.t
+      | CoercionForUntypedPhase of string
       | ArbitraryLhs
       | Continue
       | Break