feat(backend/f*): report parsing errors

engine/backends/fstar/fstar_backend.ml

@@ -111,6 +111,24 @@ module Make
 struct
   open Ctx
 
+  module StringToFStar = struct
+    let catch_parsing_error (type a b) kind span (f : a -> b) x =
+      try f x
+      with e ->
+        let kind =
+          Types.FStarParseError
+            {
+              fstar_snippet = "";
+              details =
+                "While parsing a " ^ kind ^ ", error: "
+                ^ Base.Error.to_string_hum (Base.Error.of_exn e);
+            }
+        in
+        Error.raise { span; kind }
+
+    let term span = catch_parsing_error "term" span F.term_of_string
+  end
+
   let doc_to_string : PPrint.document -> string =
     FStar_Pprint.pretty_string 1.0 (Z.of_int ctx.line_width)
 
@@ -667,7 +685,7 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
-    | Quote quote -> pquote e.span quote |> F.term_of_string
+    | Quote quote -> pquote e.span quote |> StringToFStar.term e.span
     | _ -> .
 
   (** Prints a `quote` to a string *)

hax-types/src/diagnostics/mod.rs

@@ -68,6 +68,8 @@ impl std::fmt::Display for Diagnostics {
 
             Kind::NonTrivialAndMutFnInput => write!(f, "The support in hax of function with one or more inputs of type `&mut _` is limited. Onlu trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected."),
 
+            Kind::FStarParseError { fstar_snippet, details: _ } => write!(f, "The following code snippet could not be parsed as valid F*:\n```\n{fstar_snippet}\n```"),
+
             _ => write!(f, "{:?}", self.kind),
         }
     }
@@ -135,7 +137,13 @@ pub enum Kind {
     /// An hax attribute (from `hax-lib-macros`) was rejected
     AttributeRejected {
         reason: String,
-    },
+    } = 12,
+
+    /// A snippet of F* code could not be parsed
+    FStarParseError {
+        fstar_snippet: String,
+        details: String,
+    } = 13,
 }
 
 impl Kind {