wip

.envrc

@@ -0,0 +1 @@
+use flake

cli/driver/src/exporter.rs

@@ -47,9 +47,24 @@ fn write_files(
  std::fs::write(&path, file.contents).unwrap_or_else(|e| {
  session.fatal(format!(
  "Unable to write to file {:#?}. Error: {:#?}",
- path, e
+ &path, e
  ))
- })
+ });
+ if let Some(mut sourcemap) = file.sourcemap {
+ sourcemap.inline_sources_content();
+ sourcemap.sourceRoot = manifest_dir.display().to_string();
+ let sourcemap = serde_json::to_string_pretty(&sourcemap).unwrap();
+ let path = path.with_extension(format!(
+ "{}.map",
+ path.extension().unwrap().to_str().unwrap()
+ ));
+ std::fs::write(&path, sourcemap).unwrap_or_else(|e| {
+ session.fatal(format!(
+ "Unable to write to file {:#?}. Error: {:#?}",
+ path, e
+ ))
+ });
+ }
  }
 }
 
@@ -403,6 +418,7 @@ impl Callbacks for ExtractionCallbacks {
  let engine_options = hax_cli_options_engine::EngineOptions {
  backend: backend.clone(),
  input: converted_items,
+ manifest_dir: std::env::var("CARGO_MANIFEST_DIR").unwrap().into(),
  impl_infos,
  };
  let mut engine_subprocess = find_hax_engine()

cli/options/engine/src/lib.rs

@@ -8,16 +8,46 @@ type ThirBody = hax_frontend_exporter::ThirBody;
 pub struct EngineOptions {
  pub backend: BackendOptions,
  pub input: Vec<hax_frontend_exporter::Item<ThirBody>>,
+ pub manifest_dir: String,
  pub impl_infos: Vec<(
  hax_frontend_exporter::DefId,
  hax_frontend_exporter::ImplInfos,
  )>,
 }
 
+#[allow(non_snake_case)]
+#[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)]
+pub struct SourceMap {
+ pub mappings: String,
+ pub sourceRoot: String,
+ pub sources: Vec<String>,
+ pub sourcesContent: Vec<Option<String>>,
+ pub names: Vec<String>,
+ pub version: u8,
+ pub file: String,
+}
+
+impl SourceMap {
+ pub fn inline_sources_content(&mut self) {
+ self.sourcesContent = vec![];
+ for source in &self.sources {
+ let path = if self.sourceRoot.is_empty() {
+ source.clone()
+ } else {
+ format!("{}/{}", &self.sourceRoot, source)
+ };
+ eprintln!("path={path}");
+ let contents = Some(std::fs::read_to_string(path).unwrap());
+ self.sourcesContent.push(contents);
+ }
+ }
+}
+
 #[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)]
 pub struct File {
  pub path: String,
  pub contents: String,
+ pub sourcemap: Option<SourceMap>,
 }
 
 #[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)]

engine/backends/coq/coq/coq_backend.ml

@@ -690,6 +690,7 @@ let translate _ (_bo : BackendOptions.t) (items : AST.item list) :
  path = mod_name ^ ".v";
  contents =
  hardcoded_coq_headers ^ "\n" ^ string_of_items items ^ "\n";
+ sourcemap = None;
  })
 
 open Phase_utils

engine/backends/fstar/fstar-surface-ast/FStar_String.ml

@@ -29,8 +29,8 @@ let get s i = BatUChar.code (BatUTF8.get s (Z.to_int i))
 let collect f s =
  let r = ref "" in
  BatUTF8.iter (fun c -> r := !r ^ f (BatUChar.code c)) s; !r
-let lowercase = BatString.lowercase
-let uppercase = BatString.uppercase
+let lowercase = String.lowercase_ascii
+let uppercase = String.uppercase_ascii
 let escaped = BatString.escaped
 let index = get
 exception Found of int

engine/backends/fstar/fstar_backend.ml

@@ -1213,6 +1213,8 @@ let fstar_headers (bo : BackendOptions.t) =
  in
  [ opts; "open Core"; "open FStar.Mul" ] |> String.concat ~sep:"\n"
 
+module GG = Rust_printer.Make (InputLanguage)
+
 let translate m (bo : BackendOptions.t) (items : AST.item list) :
  Types.file list =
  let show_view Concrete_ident.{ crate; path; definition } =
@@ -1227,17 +1229,25 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) :
  ~f:(map_first_letter String.uppercase)
  (fst ns :: snd ns))
  in
+ let string_of_items _ _ items =
+ let r = GG.items () items in
+ let str = Generic_printer_api.AnnotatedString.to_string r in
+ let sm = Generic_printer_api.AnnotatedString.to_sourcemap r in
+ let r = (str, sm) in
+ (r, r)
+ in
  let impl, intf = string_of_items bo m items in
- let make ~ext body =
+ let make ~ext (body, sourcemap) =
  if String.is_empty body then None
  else
  Some
  Types.
  {
  path = mod_name ^ "." ^ ext;
- contents =
- "module " ^ mod_name ^ "\n" ^ fstar_headers bo ^ "\n\n"
- ^ body ^ "\n";
+ contents = body;
+ (* "module " ^ mod_name ^ "\n" ^ fstar_headers bo ^ "\n\n" *)
+ (* ^ body ^ "\n"; *)
+ sourcemap = Some sourcemap;
  }
  in
  List.filter_map ~f:Fn.id