WIP

cryspen · Oct 8, 2024 · acd590b · acd590b
1 parent d34693e
commit acd590b
Show file tree

Hide file tree

Showing 16 changed files with 687 additions and 1,452 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -1644,6 +1644,7 @@ let fstar_headers (bo : BackendOptions.t) =
   in
   [ opts; "open Core"; "open FStar.Mul" ] |> String.concat ~sep:"\n"
 
+(*
 module GenericPrinter = Generic_rust_printer.Make (InputLanguage)
 
 (** Use the generic printer instead of the F* printer. For now, there
@@ -1684,6 +1685,7 @@ let translate_as_experimental_rust m (bo : BackendOptions.t)
                  }
          in
          List.filter_map ~f:Fn.id [ make ~ext:"rs" impl ])
+*)
 
 (** Translate as F* (the "legacy" printer) *)
 let translate_as_fstar m (bo : BackendOptions.t) (items : AST.item list) :
@@ -1728,7 +1730,7 @@ let translate =
   if
     Sys.getenv "HAX_ENGINE_EXPERIMENTAL_RUST_PRINTER_INSTEAD_OF_FSTAR"
     |> Option.is_some
-  then translate_as_experimental_rust
+  then failwith "todo"
   else translate_as_fstar
 
 open Phase_utils

diff --git a/engine/lib/dune b/engine/lib/dune
@@ -57,7 +57,7 @@
    (with-stdin-from
     %{ast}
     (run generate_visitors visitors)))))
-    
+
 (rule
  (target generated_generic_printer_base.ml)
  (deps
-Original file line number
+Diff line change
@@ Expand Up / @@ -57,7 +57,7 @@ @@
        (with-stdin-from
         %{ast}
         (run generate_visitors visitors)))))
     (rule
      (target generated_generic_printer_base.ml)
      (deps
@@ Expand Down @@