From 2f865276b504793b76d78b03056d373e9ebbe4e2 Mon Sep 17 00:00:00 2001 From: Jessica Clarke Date: Sun, 27 Sep 2020 15:22:23 +0100 Subject: [PATCH 1/4] latex: Remove unused latex_label function --- src/latex.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/latex.ml b/src/latex.ml index 6d479a527..3373e92ae 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -360,9 +360,6 @@ let rec latex_command cat id no_loc ((l, _) as annot) = ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}}" (Filename.concat !opt_directory code_file) end -let latex_label str id = - string (Printf.sprintf "\\label{%s:%s}" str (Util.zencode_string (string_of_id id))) - let counter = ref 0 let rec app_code (E_aux (exp, _)) = From 8065e4bb4a8dcd1eaa4791058bf9581b254b84da Mon Sep 17 00:00:00 2001 From: Jessica Clarke Date: Sun, 27 Sep 2020 16:35:32 +0100 Subject: [PATCH 2/4] latex: Refactor category name prefixing Rather than having the caller prefix latex and refcode strings with the category, push that down into common functions to both abstract away the details and avoid duplication. No functional change intended, and verified by regenerating the LaTeX for sail-cheri-mips and sail-cheri-riscv. --- src/latex.ml | 46 +++++++++++++++++++++++----------------------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/src/latex.ml b/src/latex.ml index 3373e92ae..0ac4097e4 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -159,7 +159,7 @@ let category_name_simple = function (* Generate a unique latex identifier from a Sail identifier. We store a mapping from identifiers to strings in state so we always return the same latex id for a sail id. *) -let latex_id id = +let latex_id_raw id = if Bindings.mem id state.generated_names then Bindings.find id state.generated_names else @@ -197,10 +197,24 @@ let latex_id id = state.generated_names <- Bindings.add id str state.generated_names; str -let refcode_string str = - Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str) +let latex_cat_id cat id = category_name cat ^ latex_id_raw id -let refcode_id id = refcode_string (string_of_id id) +let rec app_code (E_aux (exp, _)) = + match exp with + | E_app (f, [exp]) when Id.compare f (mk_id "Some") = 0 -> app_code exp + | E_app (f, [exp]) -> latex_id_raw f ^ app_code exp + | E_app (f, _) -> latex_id_raw f + | E_id id -> latex_id_raw id + | _ -> "" + +let refcode_cat_string cat str = + category_name_val cat ^ Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str) + +let refcode_cat_id prefix id = refcode_cat_string prefix (string_of_id id) + +let refcode_id = refcode_cat_id Val + +let refcode_string = refcode_cat_string Val let inline_code str = sprintf "\\lstinline{%s}" str @@ -231,7 +245,7 @@ let latex_of_markdown str = | Bold elems -> sprintf "\\textbf{%s}" (format elems) | Ref (r, "THIS", alt, _) -> begin match state.this with - | Some id -> sprintf "\\hyperref[%s]{%s}" (refcode_string (string_of_id id)) (replace_this alt) + | Some id -> sprintf "\\hyperref[%s]{%s}" (refcode_id id) (replace_this alt) | None -> failwith "Cannot create link to THIS" end | Ref (r, name, alt, _) -> @@ -337,10 +351,6 @@ let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) = let rec latex_command cat id no_loc ((l, _) as annot) = state.this <- Some id; - let labelname = match cat with - | Val -> sprintf "%s" (refcode_id id) - | _ -> sprintf "%s%s" (category_name cat) (refcode_id id) - in (* To avoid problems with verbatim environments in commands, we have to put the sail code for each command in a separate file. *) let code_file = category_name cat ^ Util.file_encode_string (string_of_id id) ^ ".tex" in @@ -348,28 +358,18 @@ let rec latex_command cat id no_loc ((l, _) as annot) = let doc = if cat = Val then no_loc else latex_loc no_loc l in output_string chan (Pretty_print_sail.to_string doc); close_out chan; - let command = sprintf "\\%s%s%s" !opt_prefix (category_name cat) (latex_id id) in + let command = sprintf "\\%s%s" !opt_prefix (latex_cat_id cat id) in if StringSet.mem command state.commands then (Reporting.warn "" l ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty) else begin state.commands <- StringSet.add command state.commands; - ksprintf string "\\newcommand{%s}{\\saildoclabelled{%s}{\\saildoc%s{" command labelname (category_name_simple cat) + ksprintf string "\\newcommand{%s}{\\saildoclabelled{%s}{\\saildoc%s{" command (refcode_cat_id cat id) (category_name_simple cat) ^^ docstring l ^^ string "}{" ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}}" (Filename.concat !opt_directory code_file) end -let counter = ref 0 - -let rec app_code (E_aux (exp, _)) = - match exp with - | E_app (f, [exp]) when Id.compare f (mk_id "Some") = 0 -> app_code exp - | E_app (f, [exp]) -> latex_id f ^ app_code exp - | E_app (f, _) -> latex_id f - | E_id id -> latex_id id - | _ -> "" - let latex_funcls def = let module StringMap = Map.Make(String) in let counter = ref 0 in @@ -495,14 +495,14 @@ let defs (Defs defs) = identifiers then outputs the correct mangled command. *) let id_command cat ids = sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat) - ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s%s}{}" (string_of_id id) !opt_prefix (category_name cat) (latex_id id)) + ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s}{}" (string_of_id id) !opt_prefix (latex_cat_id cat id)) (IdSet.elements ids) ^ "}" |> string in let ref_command cat ids = sprintf "\\newcommand{\\%sref%s}[2]{\n " !opt_prefix (category_name cat) - ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\hyperref[%s%s]{#2}}{}" (string_of_id id) (category_name_val cat) (refcode_id id)) + ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\hyperref[%s]{#2}}{}" (string_of_id id) (refcode_cat_id cat id)) (IdSet.elements ids) ^ "}" |> string From 36159bc54164916c555716123c1c63a466952db0 Mon Sep 17 00:00:00 2001 From: Jessica Clarke Date: Sun, 27 Sep 2020 16:38:03 +0100 Subject: [PATCH 3/4] latex: Prepend opt_prefix inside latex_cat_id Now that the category is prepended in latex_cat_id, also prepend opt_prefix there instead to ensure no caller forgets to do so. No functional change intended, and verified by regenerating the LaTeX for sail-cheri-mips and sail-cheri-riscv. --- src/latex.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/latex.ml b/src/latex.ml index 0ac4097e4..4abd7c6b6 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -197,7 +197,7 @@ let latex_id_raw id = state.generated_names <- Bindings.add id str state.generated_names; str -let latex_cat_id cat id = category_name cat ^ latex_id_raw id +let latex_cat_id cat id = !opt_prefix ^ category_name cat ^ latex_id_raw id let rec app_code (E_aux (exp, _)) = match exp with @@ -358,7 +358,7 @@ let rec latex_command cat id no_loc ((l, _) as annot) = let doc = if cat = Val then no_loc else latex_loc no_loc l in output_string chan (Pretty_print_sail.to_string doc); close_out chan; - let command = sprintf "\\%s%s" !opt_prefix (latex_cat_id cat id) in + let command = sprintf "\\%s" (latex_cat_id cat id) in if StringSet.mem command state.commands then (Reporting.warn "" l ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty) else @@ -495,7 +495,7 @@ let defs (Defs defs) = identifiers then outputs the correct mangled command. *) let id_command cat ids = sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat) - ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s}{}" (string_of_id id) !opt_prefix (latex_cat_id cat id)) + ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s}{}" (string_of_id id) (latex_cat_id cat id)) (IdSet.elements ids) ^ "}" |> string From 57fd06728f923d039c3f60d116f646c136528b77 Mon Sep 17 00:00:00 2001 From: Jessica Clarke Date: Sun, 27 Sep 2020 16:53:48 +0100 Subject: [PATCH 4/4] latex: Prefix label names with the specified -latex_prefix This ensures names shared between multiple projects don't collide if included in a common LaTeX document; cheri-architecture using both sail-cheri-mips and sail-cheri-riscv runs into this. Closes: #88 --- src/latex.ml | 3 ++- src/sail.ml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/latex.ml b/src/latex.ml index 4abd7c6b6..c59d83677 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -208,7 +208,8 @@ let rec app_code (E_aux (exp, _)) = | _ -> "" let refcode_cat_string cat str = - category_name_val cat ^ Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str) + let refcode_str = Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str) in + !opt_prefix ^ category_name_val cat ^ refcode_str let refcode_cat_id prefix id = refcode_cat_string prefix (string_of_id id) diff --git a/src/sail.ml b/src/sail.ml index d07ea216e..53a5cc5d5 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -162,7 +162,7 @@ let options = Arg.align ([ " pretty print the input to LaTeX"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix := prefix), - " set a custom prefix for generated LaTeX macro command (default sail)"); + " set a custom prefix for generated LaTeX labels and macro commands (default sail)"); ( "-latex_full_valspecs", Arg.Clear Latex.opt_simple_val, " print full valspecs in LaTeX output");