From ca69f1c021d9b647abef95b79de9641cca61be50 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Sun, 8 Sep 2024 18:56:13 -0700
Subject: [PATCH] ExtractSteel: update for new F* error API

---
 src/extraction/ExtractSteel.fst            | 10 +++---
 src/ocaml/plugin/generated/ExtractSteel.ml | 40 ++++++++++------------
 2 files changed, 24 insertions(+), 26 deletions(-)

diff --git a/src/extraction/ExtractSteel.fst b/src/extraction/ExtractSteel.fst
index 2fcbbc562..7f70dca70 100644
--- a/src/extraction/ExtractSteel.fst
+++ b/src/extraction/ExtractSteel.fst
@@ -164,14 +164,13 @@ let steel_translate_expr : translate_expr_t = fun env e ->
   | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_fp; _fp'; _opened; _p; _i; e])
     when string_of_mlpath p = "Steel.ST.Util.with_invariant" ||
          string_of_mlpath p = "Steel.Effect.Atomic.with_invariant" ->
-    Errors.raise_error
-      (Errors.Fatal_ExtractionUnsupported,
-       BU.format2
+    Errors.raise_error0
+      Errors.Fatal_ExtractionUnsupported
+      (BU.format2
          "Extraction of with_invariant requires its argument to be a function literal \
          at extraction time, try marking its argument inline_for_extraction (%s, %s)"
          (string_of_int (fst e.loc))
          (snd e.loc))
-      Range.dummyRange
 
   | _ -> raise NotSupportedByKrmlExtension
 
@@ -197,7 +196,8 @@ let steel_translate_let : translate_let_t = fun env flavor lb ->
         let expr = List.map (translate_expr env) (list_elements l) in
         Some (DGlobal (meta, name, List.length tvars, t, EBufCreateL (Eternal, expr)))
       with e ->
-          Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format2 "Error extracting %s to KaRaMeL (%s)\n" (Syntax.string_of_mlpath name) (BU.print_exn e)));
+          Errors.log_issue0 Errors.Warning_DefinitionNotTranslated
+            (BU.format2 "Error extracting %s to KaRaMeL (%s)\n" (Syntax.string_of_mlpath name) (BU.print_exn e));
           Some (DGlobal (meta, name, List.length tvars, t, EAny))
         end
     | _ -> raise NotSupportedByKrmlExtension
diff --git a/src/ocaml/plugin/generated/ExtractSteel.ml b/src/ocaml/plugin/generated/ExtractSteel.ml
index d33a26ecf..2dcd98afe 100644
--- a/src/ocaml/plugin/generated/ExtractSteel.ml
+++ b/src/ocaml/plugin/generated/ExtractSteel.ml
@@ -579,18 +579,17 @@ let (steel_translate_expr : FStar_Extraction_Krml.translate_expr_t) =
           ->
           let uu___5 =
             let uu___6 =
-              let uu___7 =
-                FStar_Compiler_Util.string_of_int
-                  (FStar_Pervasives_Native.fst
-                     e2.FStar_Extraction_ML_Syntax.loc) in
-              FStar_Compiler_Util.format2
-                "Extraction of with_invariant requires its argument to be a function literal at extraction time, try marking its argument inline_for_extraction (%s, %s)"
-                uu___7
-                (FStar_Pervasives_Native.snd
+              FStar_Compiler_Util.string_of_int
+                (FStar_Pervasives_Native.fst
                    e2.FStar_Extraction_ML_Syntax.loc) in
-            (FStar_Errors_Codes.Fatal_ExtractionUnsupported, uu___6) in
-          FStar_Errors.raise_error uu___5
-            FStar_Compiler_Range_Type.dummyRange
+            FStar_Compiler_Util.format2
+              "Extraction of with_invariant requires its argument to be a function literal at extraction time, try marking its argument inline_for_extraction (%s, %s)"
+              uu___6
+              (FStar_Pervasives_Native.snd e2.FStar_Extraction_ML_Syntax.loc) in
+          FStar_Errors.raise_error0
+            FStar_Errors_Codes.Fatal_ExtractionUnsupported ()
+            (Obj.magic FStar_Errors_Msg.is_error_message_string)
+            (Obj.magic uu___5)
       | uu___ ->
           FStar_Compiler_Effect.raise
             FStar_Extraction_Krml.NotSupportedByKrmlExtension
@@ -661,16 +660,15 @@ let (steel_translate_let : FStar_Extraction_Krml.translate_let_t) =
                | uu___11 ->
                    ((let uu___13 =
                        let uu___14 =
-                         let uu___15 =
-                           FStar_Extraction_ML_Syntax.string_of_mlpath name1 in
-                         let uu___16 = FStar_Compiler_Util.print_exn uu___11 in
-                         FStar_Compiler_Util.format2
-                           "Error extracting %s to KaRaMeL (%s)\n" uu___15
-                           uu___16 in
-                       (FStar_Errors_Codes.Warning_DefinitionNotTranslated,
-                         uu___14) in
-                     FStar_Errors.log_issue
-                       FStar_Compiler_Range_Type.dummyRange uu___13);
+                         FStar_Extraction_ML_Syntax.string_of_mlpath name1 in
+                       let uu___15 = FStar_Compiler_Util.print_exn uu___11 in
+                       FStar_Compiler_Util.format2
+                         "Error extracting %s to KaRaMeL (%s)\n" uu___14
+                         uu___15 in
+                     FStar_Errors.log_issue0
+                       FStar_Errors_Codes.Warning_DefinitionNotTranslated ()
+                       (Obj.magic FStar_Errors_Msg.is_error_message_string)
+                       (Obj.magic uu___13));
                     FStar_Pervasives_Native.Some
                       (FStar_Extraction_Krml.DGlobal
                          (meta1, name1, (FStar_Compiler_List.length tvars),