Merge PR #8565: Make coqpp handle OCaml locations

3 files changed, 22 insertions, 11 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 181c43615b..956a916792 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -11,7 +11,7 @@ type loc = {
   loc_end : Lexing.position;
 }
 
-type code = { code : string }
+type code = { code : string; loc : loc; }
 
 type user_symbol =
 | Ulist1 of user_symbol
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index bfa4e2b57b..81a53e887b 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -29,6 +29,7 @@ let newline lexbuf =
 
 let num_comments = ref 0
 let num_braces = ref 0
+let ocaml_start_pos = ref Lexing.dummy_pos
 
 let mode () = if !num_braces = 0 then Extend else OCaml
 
@@ -57,10 +58,10 @@ let end_comment lexbuf =
   else
     None
 
-let start_ocaml _ =
+let start_ocaml lexbuf =
   let () = match mode () with
   | OCaml -> Buffer.add_string ocaml_buf "{"
-  | Extend -> ()
+  | Extend -> ocaml_start_pos := lexeme_start_p lexbuf
   in
   incr num_braces
 
@@ -70,7 +71,11 @@ let end_ocaml lexbuf =
   else if !num_braces = 0 then
     let s = Buffer.contents ocaml_buf in
     let () = Buffer.reset ocaml_buf in
-    Some (CODE { Coqpp_ast.code = s })
+    let loc = {
+      Coqpp_ast.loc_start = !ocaml_start_pos;
+      Coqpp_ast.loc_end = lexeme_end_p lexbuf
+    } in
+    Some (CODE { Coqpp_ast.code = s; loc })
   else
     let () = Buffer.add_string ocaml_buf "}" in
     None
@@ -87,7 +92,7 @@ let number = [ '0'-'9' ]
 
 rule extend = parse
 | "(*" { start_comment (); comment lexbuf }
-| "{" { start_ocaml (); ocaml lexbuf }
+| "{" { start_ocaml lexbuf; ocaml lexbuf }
 | "GRAMMAR" { GRAMMAR }
 | "VERNAC" { VERNAC }
 | "TACTIC" { TACTIC }
@@ -127,7 +132,7 @@ rule extend = parse
 | eof { EOF }
 
 and ocaml = parse
-| "{" { start_ocaml (); ocaml lexbuf }
+| "{" { start_ocaml lexbuf; ocaml lexbuf }
 | "}" { match end_ocaml lexbuf with Some tk -> tk | None -> ocaml lexbuf }
 | '\n' { newline lexbuf; Buffer.add_char ocaml_buf '\n'; ocaml lexbuf }
 | '\"' { Buffer.add_char ocaml_buf '\"'; ocaml_string lexbuf }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index a8ed95f5ba..d9fff46d88 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -21,6 +21,13 @@ let pr_loc loc =
   let epos = loc.loc_end.pos_cnum - loc.loc_start.pos_bol in
   Printf.sprintf "File \"%s\", line %d, characters %d-%d:" file line bpos epos
 
+let print_code fmt c =
+  let loc = c.loc.loc_start in
+  (** Print the line location as a source annotation *)
+  let padding = String.make (loc.pos_cnum - loc.pos_bol + 1) ' ' in
+  let code_insert = asprintf "\n# %i \"%s\"\n%s%s" loc.pos_lnum loc.pos_fname padding c.code in
+  fprintf fmt "@[@<0>%s@]@\n" code_insert
+
 let parse_file f =
   let chan = open_in f in
   let lexbuf = Lexing.from_channel chan in
@@ -181,8 +188,7 @@ let print_fun fmt (vars, body) =
   in
   let () = fprintf fmt "fun@ " in
   let () = List.iter iter vars in
-  (* FIXME: use Coq locations in the macros *)
-  let () = fprintf fmt "loc ->@ @[%s@]" body.code in
+  let () = fprintf fmt "loc ->@ @[%a@]" print_code body in
   ()
 
 (** Meta-program instead of calling Tok.of_pattern here because otherwise
@@ -304,8 +310,8 @@ let rec print_binders fmt = function
   fprintf fmt "%s@ %a" id print_binders rem
 
 let print_rule fmt r =
-  fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]"
-    print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code
+  fprintf fmt "@[TyML (%a, @[fun %a -> %a@])@]"
+    print_clause r.tac_toks print_binders r.tac_toks print_code r.tac_body
 
 let rec print_rules fmt = function
 | [] -> ()
@@ -338,7 +344,7 @@ let declare_plugin fmt name =
   fprintf fmt "let _ = Mltop.add_known_module %s@\n" plugin_name
 
 let pr_ast fmt = function
-| Code s -> fprintf fmt "%s@\n" s.code
+| Code s -> fprintf fmt "%a@\n" print_code s
 | Comment s -> fprintf fmt "%s@\n" s
 | DeclarePlugin name -> declare_plugin fmt name
 | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram