Merge pull request #1123 from hacspec/coq-sourcemaps

Engine: source maps: fix bugs, add features, enable for Coq

cli/subcommands/src/cargo_hax.rs

@@ -332,6 +332,27 @@ fn run_engine(
                             std::fs::write(&path, file.contents).unwrap();
                             wrote = true;
                         }
+                        if let Some(mut sourcemap) = file.sourcemap.clone() {
+                            sourcemap.sourcesContent = sourcemap
+                                .sources
+                                .iter()
+                                .map(PathBuf::from)
+                                .map(|path| {
+                                    if path.is_absolute() {
+                                        path
+                                    } else {
+                                        working_dir.join(path).to_path_buf()
+                                    }
+                                })
+                                .map(|path| fs::read_to_string(path).ok())
+                                .collect();
+                            let f = std::fs::File::create(path.with_file_name(format!(
+                                "{}.map",
+                                path.file_name().unwrap().to_string_lossy()
+                            )))
+                            .unwrap();
+                            serde_json::to_writer(std::io::BufWriter::new(f), &sourcemap).unwrap()
+                        }
                         HaxMessage::ProducedFile { path, wrote }.report(message_format, None)
                     }
                 }

engine/backends/coq/coq/coq_backend.ml

@@ -767,13 +767,16 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list =
                 ~f:(map_first_letter String.uppercase)
                 (fst ns :: snd ns))
          in
-         let contents, _annotations = my_printer#entrypoint_modul items in
-         Types.
-           {
-             path = mod_name ^ ".v";
-             contents = hardcoded_coq_headers ^ "\n" ^ contents;
-             sourcemap = None;
-           })
+         let sourcemap, contents =
+           let annotated = my_printer#entrypoint_modul items in
+           let open Generic_printer.AnnotatedString in
+           let header = pure (hardcoded_coq_headers ^ "\n") in
+           let annotated = concat header annotated in
+           (to_sourcemap annotated, to_string annotated)
+         in
+         let sourcemap = Some sourcemap in
+         let path = mod_name ^ ".v" in
+         Types.{ path; contents; sourcemap })
 
 open Phase_utils
 

engine/lib/generic_printer/generic_printer.ml

@@ -74,6 +74,29 @@ module AnnotatedString = struct
   let to_spanned_strings ((s, annots) : t) : (Ast.span * string) list =
     Annotation.split_with_string s annots
 
+  (** Lifts a string to an annotated list *)
+  let pure (s : string) : t = (s, [])
+
+  (** Concatenate two annotated strings *)
+  let concat (x : t) (y : t) : t =
+    let (xs, xl), (ys, yl) = (x, y) in
+    let last_x =
+      let lines = String.split ~on:'\n' xs in
+      let last_line = List.last lines |> Option.value ~default:"" in
+      let col, line = (String.length last_line, List.length lines) in
+      Annotation.{ col; line }
+    in
+    let yl =
+      let f ({ line; col } : Annotation.loc) : Annotation.loc =
+        {
+          line = line + last_x.line;
+          col = (match col with 0 -> col + last_x.col | _ -> col);
+        }
+      in
+      List.map ~f:(f *** Fn.id) yl
+    in
+    (xs ^ ys, xl @ yl)
+
   let to_sourcemap : t -> Types.source_map =
     snd >> List.filter_map ~f:Annotation.to_mapping >> Sourcemaps.Source_maps.mk
     >> fun ({
@@ -90,7 +113,7 @@ module AnnotatedString = struct
       { mappings; sourceRoot; sources; sourcesContent; names; version; file }
 end
 
-(** Helper class that brings imperative span  *)
+(** Helper class that brings imperative span *)
 class span_helper : object
   method span_data : Annotation.t list
   (** Get the span annotation accumulated while printing *)

engine/utils/sourcemaps/location.ml

@@ -1,6 +1,6 @@
 open Prelude
 
-type t = { line : int; col : int } [@@deriving eq]
+type t = { line : int; col : int } [@@deriving eq, yojson]
 
 let show { line; col } =
   "(" ^ Int.to_string line ^ ":" ^ Int.to_string col ^ ")"

engine/utils/sourcemaps/mappings/dual.ml

@@ -1,4 +1,4 @@
-type 'a t = { gen : 'a; src : 'a } [@@deriving show, eq]
+type 'a t = { gen : 'a; src : 'a } [@@deriving show, eq, yojson]
 
 let transpose ~(default : 'a t) ({ gen; src } : 'a option t) : 'a t option =
   match (gen, src) with

engine/utils/sourcemaps/mappings/instruction.ml

@@ -8,9 +8,7 @@ type t =
 [@@deriving show { with_path = false }, eq]
 
 let encode_one : t -> string * [ `Sep | `NeedsSep ] = function
-  | ShiftGenLinesResetGenCols { lines } ->
-      Stdlib.prerr_endline ("lines:::" ^ Int.to_string lines);
-      (String.make lines ';', `Sep)
+  | ShiftGenLinesResetGenCols { lines } -> (String.make lines ';', `Sep)
   | ShiftGenCols n -> (Vql.encode_base64 [ n ], `NeedsSep)
   | Full { shift_gen_col; shift_src; meta = { file_offset; name } } ->
       ( Vql.encode_base64
@@ -75,23 +73,32 @@ let to_points ?(init = Dual.default Location.default) : t list -> point list =
   >> snd >> List.rev
 
 let from_points : point list -> t list =
-  List.folding_map ~init:(Dual.default Location.default)
-    ~f:(fun { src; gen } (x, m) ->
+  List.folding_map
+    ~init:(Dual.default Location.default, None)
+    ~f:(fun ({ src; gen }, m0) (x, m) ->
       let d =
         Location.(Dual.{ Dual.src = x.src - src; Dual.gen = x.gen - gen })
       in
       let shift_gen_col = (if Int.(d.gen.line = 0) then d else x).gen.col in
+      let relative_m =
+        Option.map m ~f:(fun m ->
+            match m0 with
+            | Some m0 ->
+                { file_offset = m.file_offset - m0.file_offset; name = None }
+            | None -> m)
+      in
       let output =
         (if Int.(d.gen.line = 0) then []
          else [ ShiftGenLinesResetGenCols { lines = d.gen.line } ])
         @
-        match m with
+        match relative_m with
         | Some meta -> [ Full { shift_gen_col; shift_src = d.src; meta } ]
         | None when Int.(shift_gen_col = 0) -> []
+        | _ when Int.(shift_gen_col = 0) -> []
         | _ -> [ ShiftGenCols shift_gen_col ]
       in
       let x = match m with Some _ -> x | None -> { x with src } in
-      (x, output))
+      ((x, Option.first_some m m0), output))
   >> List.concat
 
 let%test _ =

engine/utils/sourcemaps/mappings/mappings.ml

@@ -2,10 +2,11 @@ open Prelude
 include Types
 
 type range = { start : Location.t; end_ : Location.t option }
-[@@deriving show, eq]
+[@@deriving show, eq, yojson]
 
 module Chunk = struct
-  type t = { gen : range; src : range; meta : meta } [@@deriving show, eq]
+  type t = { gen : range; src : range; meta : meta }
+  [@@deriving show, eq, yojson]
 
   let compare (x : t) (y : t) = Location.compare x.gen.start y.gen.start
 

engine/utils/sourcemaps/mappings/mappings.mli

@@ -1,8 +1,12 @@
-type meta = { file_offset : int; name : int option } [@@deriving show, eq]
+type meta = { file_offset : int; name : int option }
+[@@deriving show, eq, yojson]
+
 type range = { start : Location.t; end_ : Location.t option }
+[@@deriving show, eq, yojson]
 
 module Chunk : sig
-  type t = { gen : range; src : range; meta : meta } [@@deriving show, eq]
+  type t = { gen : range; src : range; meta : meta }
+  [@@deriving show, eq, yojson]
 
   val compare : t -> t -> int
 end

engine/utils/sourcemaps/mappings/types.ml

@@ -1,4 +1,6 @@
 open Prelude
 
-type meta = { file_offset : int; name : int option } [@@deriving show, eq]
-type point = Location.t Dual.t * meta option [@@deriving show, eq]
+type meta = { file_offset : int; name : int option }
+[@@deriving show, eq, yojson]
+
+type point = Location.t Dual.t * meta option [@@deriving show, eq, yojson]

engine/utils/sourcemaps/source_maps.ml

@@ -45,7 +45,6 @@ let mk ?(file = "") ?(sourceRoot = "") ?(sourcesContent = fun _ -> None)
     Chunk.{ gen; src; meta }
   in
   let mappings = List.map mappings ~f |> List.sort ~compare:Chunk.compare in
-  Stdlib.prerr_endline @@ [%show: Chunk.t list] mappings;
   let mappings = Mappings.encode mappings in
   let sourcesContent = List.map ~f:sourcesContent sources in
   { mappings; sourceRoot; sourcesContent; sources; names; version = 3; file }