From 564f7106932374a90a4d2ba97830f3209abdf66a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9lio=20Brun?= Date: Fri, 17 Jan 2025 17:11:11 +0900 Subject: [PATCH 1/3] Add a LaTeX `\ottfirstprodnewline` command for the newline after a rule head. In custom setups, this enables merging the head line with the first production line. --- src/grammar_pp.ml | 40 ++++++++++++++++++++++------------------ src/system_pp.ml | 1 + 2 files changed, 23 insertions(+), 18 deletions(-) diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 6743c20..201af23 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -771,6 +771,7 @@ let pp_tex_BINDSPEC_PROD_NAME m = "\\"^pp_tex_NAME_PREFIX m^"bindspecprod let pp_tex_FIRST_LONG_PROD_NAME m = "\\"^pp_tex_NAME_PREFIX m^"firstlongprodline" let pp_tex_FIRST_PROD_NAME m = "\\"^pp_tex_NAME_PREFIX m^"firstprodline" let pp_tex_PROD_NEWLINE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"prodnewline" +let pp_tex_FIRST_PROD_NEWLINE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"firstprodnewline" let pp_tex_INTERRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"interrule" let pp_tex_AFTERLASTRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"afterlastrule" @@ -2678,24 +2679,27 @@ and pp_rule m xd r = (* returns a string option *) else Some (* TODO: update the following to respect pp_tex_LONG_PROD_NAME (if necessary...) *) - (Str.replace_first - (Str.regexp_string (pp_tex_PROD_NAME m)) - (pp_tex_FIRST_PROD_NAME m) - ( "\\newcommand{" - ^ tex_rule_name m r.rule_ntr_name - ^ "}{\n" - ^ (String.concat (pp_tex_PROD_NEWLINE_NAME m^"\n") - ( ( pp_tex_RULEHEAD_NAME m^"{" - ^ String.concat " ,\\ " - (Auxl.remove_duplicates (List.map (function ntr,homs->pp_nontermroot m xd ntr) r.rule_ntr_names)) - ^ "}{::=}{" ^ pp_com ^ "}") - :: - (Auxl.option_map - (pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper) - r.rule_ps))) -(* ^"[5.0mm]" *) - ^ "}\n" )) - in + (Str.replace_first + (Str.regexp_string (pp_tex_PROD_NEWLINE_NAME m)) + (pp_tex_FIRST_PROD_NEWLINE_NAME m) + (Str.replace_first + (Str.regexp_string (pp_tex_PROD_NAME m)) + (pp_tex_FIRST_PROD_NAME m) + ( "\\newcommand{" + ^ tex_rule_name m r.rule_ntr_name + ^ "}{\n" + ^ (String.concat (pp_tex_PROD_NEWLINE_NAME m^"\n") + ( ( pp_tex_RULEHEAD_NAME m^"{" + ^ String.concat " ,\\ " + (Auxl.remove_duplicates (List.map (function ntr,homs->pp_nontermroot m xd ntr) r.rule_ntr_names)) + ^ "}{::=}{" ^ pp_com ^ "}") + :: + (Auxl.option_map + (pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper) + r.rule_ps))) + (* ^"[5.0mm]" *) + ^ "}\n" ))) + in match result with | Some s -> Some (if !Global_option.output_source_locations >= 2 then "\n"^pp_source_location m r.rule_loc ^ s else s) | None -> None diff --git a/src/system_pp.ml b/src/system_pp.ml index 88f3b2e..10fbd35 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -586,6 +586,7 @@ let pp_systemdefn_core_tex m sd lookup oi = Printf.fprintf fd ("\\newcommand{%s}[6]{%s{#1}{#2}{#3}{#4}{#5}{#6}}\n") (Grammar_pp.pp_tex_BINDSPEC_PROD_NAME m ) (Grammar_pp.pp_tex_PROD_NAME m); Printf.fprintf fd ("\\newcommand{%s}{\\\\}\n") (Grammar_pp.pp_tex_PROD_NEWLINE_NAME m ); + Printf.fprintf fd ("\\newcommand{%s}{\\\\}\n") (Grammar_pp.pp_tex_FIRST_PROD_NEWLINE_NAME m ); Printf.fprintf fd ("\\newcommand{%s}{\\\\[5.0mm]}\n") (Grammar_pp.pp_tex_INTERRULE_NAME m ); Printf.fprintf fd ("\\newcommand{%s}{\\\\}\n") (Grammar_pp.pp_tex_AFTERLASTRULE_NAME m ); Embed_pp.pp_embeds fd m sd.syntax lookup sd.syntax.xd_embed_preamble; From dc3bce6265ca2aad1465716c1b1468f712992a04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9lio=20Brun?= Date: Mon, 20 Jan 2025 15:29:44 +0900 Subject: [PATCH 2/3] Generates a special command for the last premise of a rule to allow avoiding the generation of an unwanted separator --- src/defns.ml | 8 ++++++-- src/grammar_pp.ml | 1 + src/system_pp.ml | 1 + 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/defns.ml b/src/defns.ml index 90727f6..684b1b2 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -236,8 +236,12 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = Printf.fprintf fd "\\newcommand{%s}[1]{%s[#1]{%%\n" (Grammar_pp.tex_drule_name m dr.drule_name) (Grammar_pp.pp_tex_DRULE_NAME m); - List.iter - (fun p-> Printf.fprintf fd "%s{%s}%%\n" (Grammar_pp.pp_tex_PREMISE_NAME m) p) + let n = List.length (snd ppd_premises) in + List.iteri + (fun i p -> + Printf.fprintf fd "%s{%s}%%\n" + (if i = n - 1 then Grammar_pp.pp_tex_LAST_PREMISE_NAME m + else Grammar_pp.pp_tex_PREMISE_NAME m) p) (snd ppd_premises); output_string fd "}{\n"; output_string fd ppd_conclusion; diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 201af23..e48b377 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -786,6 +786,7 @@ let pp_tex_DRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"drule" let pp_tex_DRULE_NAME_NAME m = "\\"^pp_tex_NAME_PREFIX m^"drulename" let pp_tex_USE_DRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"usedrule" let pp_tex_PREMISE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"premise" +let pp_tex_LAST_PREMISE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"lastpremise" let pp_tex_DEFN_BLOCK_NAME m = pp_tex_NAME_PREFIX m^"defnblock" let pp_tex_FUNCLAUSE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"funclause" let pp_tex_FUNDEFN_BLOCK_NAME m = pp_tex_NAME_PREFIX m^"fundefnblock" diff --git a/src/system_pp.ml b/src/system_pp.ml index 10fbd35..86318c2 100644 --- a/src/system_pp.ml +++ b/src/system_pp.ml @@ -557,6 +557,7 @@ let pp_systemdefn_core_tex m sd lookup oi = (Grammar_pp.pp_tex_DRULE_NAME m) (Grammar_pp.pp_tex_DRULE_NAME_NAME m); Printf.fprintf fd ("\\newcommand{%s}[1]{\\[#1\\]}\n") (Grammar_pp.pp_tex_USE_DRULE_NAME m); Printf.fprintf fd ("\\newcommand{%s}[1]{ #1 \\\\}\n") (Grammar_pp.pp_tex_PREMISE_NAME m ); + Printf.fprintf fd ("\\newcommand{%s}[1]{ #1 \\\\}\n") (Grammar_pp.pp_tex_LAST_PREMISE_NAME m ); Printf.fprintf fd ("\\newenvironment{%s}[3][]{ \\framebox{\\mbox{#2}} \\quad #3 \\\\[0pt]}{}\n") (Grammar_pp.pp_tex_DEFN_BLOCK_NAME m ); Printf.fprintf fd ("\\newenvironment{%s}[3][]{ \\framebox{\\mbox{#2}} \\quad #3 \\\\[0pt]\\begin{displaymath}\\begin{array}{l}}{\\end{array}\\end{displaymath}}\n") (Grammar_pp.pp_tex_FUNDEFN_BLOCK_NAME m ); From 5e40781fbf268472e73af6cdfdc66a3b749db9ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9lio=20Brun?= Date: Wed, 22 Jan 2025 20:49:28 +0900 Subject: [PATCH 3/3] add a command for rules names --- src/defns.ml | 9 ++++++--- src/grammar_pp.ml | 1 + 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/defns.ml b/src/defns.ml index 684b1b2..4a16e93 100644 --- a/src/defns.ml +++ b/src/defns.ml @@ -233,6 +233,10 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = "\\text{" ^ String.concat "" (Grammar_pp.apply_hom_spec m xd hs []) ^ "}") in + Printf.fprintf fd "\\newcommand{%s}{%s{%s}}\n" + (Grammar_pp.tex_drule_name_name m dr.drule_name) + (Grammar_pp.pp_tex_DRULE_NAME_NAME m) + (Auxl.pp_tex_escape dr.drule_name); Printf.fprintf fd "\\newcommand{%s}[1]{%s[#1]{%%\n" (Grammar_pp.tex_drule_name m dr.drule_name) (Grammar_pp.pp_tex_DRULE_NAME m); @@ -245,9 +249,8 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit = (snd ppd_premises); output_string fd "}{\n"; output_string fd ppd_conclusion; - Printf.fprintf fd "}{%%\n{%s{%s}}{%s}%%\n}}\n" - (Grammar_pp.pp_tex_DRULE_NAME_NAME m) - (Auxl.pp_tex_escape dr.drule_name) + Printf.fprintf fd "}{%%\n{%s}{%s}%%\n}}\n" + (Grammar_pp.tex_drule_name_name m dr.drule_name) pp_com | Isa _ | Hol _ | Lem _ | Coq _ | Twf _ -> let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index e48b377..f58e510 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -820,6 +820,7 @@ let rec tex_command_escape s = (Auxl.char_list_of_string s)) and tex_rule_name m ntr = "\\"^pp_tex_NAME_PREFIX m^tex_command_escape ntr +and tex_drule_name_name m s = "\\"^pp_tex_NAME_PREFIX m^"drulename"^tex_command_escape s and tex_drule_name m s = "\\"^pp_tex_NAME_PREFIX m^"drule"^tex_command_escape s and tex_defn_name m wrapper s = "\\"^pp_tex_NAME_PREFIX m^"defn"^tex_command_escape (wrapper^s) and tex_defnclass_name m s = "\\"^pp_tex_NAME_PREFIX m^"defns"^tex_command_escape s