summaryrefslogtreecommitdiff
path: root/tools/coq_tex.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coq_tex.ml')
-rw-r--r--tools/coq_tex.ml295
1 files changed, 295 insertions, 0 deletions
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
new file mode 100644
index 00000000..350b59aa
--- /dev/null
+++ b/tools/coq_tex.ml
@@ -0,0 +1,295 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* coq-tex
+ * JCF, 16/1/98
+ * adapted from caml-tex (perl script written by Xavier Leroy)
+ *
+ * Perl isn't as portable as it pretends to be, and is quite difficult
+ * to read and maintain... Let us rewrite the stuff in Caml! *)
+
+let linelen = ref 72
+let output = ref ""
+let output_specified = ref false
+let image = ref ""
+let cut_at_blanks = ref false
+let verbose = ref false
+let slanted = ref false
+let hrule = ref false
+let small = ref false
+let boot = ref false
+
+let coq_prompt = Str.regexp "Coq < "
+let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
+
+let remove_prompt s = Str.replace_first any_prompt "" s
+
+(* First pass: extract the Coq phrases to evaluate from [texfile]
+ * and put them into the file [inputv] *)
+
+let begin_coq = Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
+let end_coq = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
+
+let extract texfile inputv =
+ let chan_in = open_in texfile in
+ let chan_out = open_out inputv in
+ let rec inside () =
+ let s = input_line chan_in in
+ if Str.string_match end_coq s 0 then
+ outside ()
+ else begin
+ output_string chan_out (s ^ "\n");
+ inside ()
+ end
+ and outside () =
+ let s = input_line chan_in in
+ if Str.string_match begin_coq s 0 then
+ inside ()
+ else
+ outside ()
+ in
+ try
+ output_string chan_out
+ ("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
+ outside ()
+ with End_of_file ->
+ begin close_in chan_in; close_out chan_out end
+
+(* Second pass: insert the answers of Coq from [coq_output] into the
+ * TeX file [texfile]. The result goes in file [result]. *)
+
+let begin_coq_example =
+ Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
+let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
+let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
+let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
+let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
+
+let has_match r s =
+ try let _ = Str.search_forward r s 0 in true with Not_found -> false
+
+let percent = Str.regexp "%"
+let bang = Str.regexp "!"
+let expos = Str.regexp "^"
+
+let tex_escaped s =
+ let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in
+ let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in
+ let adapt_delim = function
+ | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+ | "\\" -> "{\\char'134}"
+ | "^" -> "{\\char'136}"
+ | "~" -> "{\\char'176}"
+ | " " -> "~"
+ | "<" -> "{<}"
+ | ">" -> "{>}"
+ | _ -> assert false
+ in
+ let adapt = function
+ | Str.Text s -> s
+ | Str.Delim s -> adapt_delim s
+ in
+ String.concat "" (List.map adapt (Str.full_split delims s))
+
+let encapsule sl c_out s =
+ if sl then
+ Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s)
+ else
+ Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s)
+
+let print_block c_out bl =
+ List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl
+
+let insert texfile coq_output result =
+ let c_tex = open_in texfile in
+ let c_coq = open_in coq_output in
+ let c_out = open_out result in
+ (* next_block k : this function reads the next block of Coq output
+ * removing the k leading prompts.
+ * it returns the block as a list of string) *)
+ let last_read = ref "" in
+ let next_block k =
+ if !last_read = "" then last_read := input_line c_coq;
+ (* skip k prompts *)
+ for i = 1 to k do
+ last_read := remove_prompt !last_read;
+ done;
+ (* read and return the following lines until a prompt is found *)
+ let rec read_lines () =
+ let s = input_line c_coq in
+ if Str.string_match any_prompt s 0 then begin
+ last_read := s; []
+ end else
+ s :: (read_lines ())
+ in
+ let first = !last_read in first :: (read_lines ())
+ in
+ (* we are just after \end{coq_...} block *)
+ let rec just_after () =
+ let s = input_line c_tex in
+ if Str.string_match begin_coq_example s 0 then begin
+ inside (Str.matched_group 1 s <> "example*")
+ (Str.matched_group 1 s <> "example#") 0 false
+ end
+ else begin
+ if !hrule then output_string c_out "\\hrulefill\\\\\n";
+ output_string c_out "\\end{flushleft}\n";
+ if !small then output_string c_out "\\end{small}\n";
+ if Str.string_match begin_coq_eval s 0 then
+ eval 0
+ else begin
+ output_string c_out (s ^ "\n");
+ outside ()
+ end
+ end
+ (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
+ and outside () =
+ let s = input_line c_tex in
+ if Str.string_match begin_coq_example s 0 then begin
+ if !small then output_string c_out "\\begin{small}\n";
+ output_string c_out "\\begin{flushleft}\n";
+ if !hrule then output_string c_out "\\hrulefill\\\\\n";
+ inside (Str.matched_group 1 s <> "example*")
+ (Str.matched_group 1 s <> "example#") 0 true
+ end else if Str.string_match begin_coq_eval s 0 then
+ eval 0
+ else begin
+ output_string c_out (s ^ "\n");
+ outside ()
+ end
+ (* we are inside a \begin{coq_example?} ... \end{coq_example?} block
+ * show_answers tells what kind of block it is
+ * k is the number of lines read until now *)
+ and inside show_answers show_questions k first_block =
+ let s = input_line c_tex in
+ if Str.string_match end_coq_example s 0 then begin
+ just_after ()
+ end else begin
+ if !verbose then Printf.printf "Coq < %s\n" s;
+ if (not first_block) & k=0 then output_string c_out "\\medskip\n";
+ if show_questions then encapsule false c_out ("Coq < " ^ s);
+ if has_match dot_end_line s then begin
+ let bl = next_block (succ k) in
+ if !verbose then List.iter print_endline bl;
+ if show_answers then print_block c_out bl;
+ inside show_answers show_questions 0 false
+ end else
+ inside show_answers show_questions (succ k) first_block
+ end
+ (* we are inside a \begin{coq_eval} ... \end{coq_eval} block
+ * k is the number of lines read until now *)
+ and eval k =
+ let s = input_line c_tex in
+ if Str.string_match end_coq_eval s 0 then
+ outside ()
+ else begin
+ if !verbose then Printf.printf "Coq < %s\n" s;
+ if has_match dot_end_line s then
+ let bl = next_block (succ k) in
+ if !verbose then List.iter print_endline bl;
+ eval 0
+ else
+ eval (succ k)
+ end
+ in
+ try
+ let _ = next_block 0 in (* to skip the Coq banner *)
+ let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *)
+ outside ()
+ with End_of_file -> begin
+ close_in c_tex;
+ close_in c_coq;
+ close_out c_out
+ end
+
+(* Process of one TeX file *)
+
+let rm f = try Sys.remove f with _ -> ()
+
+let one_file texfile =
+ let inputv = Filename.temp_file "coq_tex" ".v" in
+ let coq_output = Filename.temp_file "coq_tex" ".coq_output"in
+ let result =
+ if !output_specified then
+ !output
+ else if Filename.check_suffix texfile ".tex" then
+ (Filename.chop_suffix texfile ".tex") ^ ".v.tex"
+ else
+ texfile ^ ".v.tex"
+ in
+ try
+ (* 1. extract Coq phrases *)
+ extract texfile inputv;
+ (* 2. run Coq on input *)
+ let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv
+ coq_output)
+ in
+ (* 3. insert Coq output into original file *)
+ insert texfile coq_output result;
+ (* 4. clean up *)
+ rm inputv; rm coq_output
+ with e -> begin
+ rm inputv; rm coq_output;
+ raise e
+ end
+
+(* Parsing of the command line, check of the Coq command and process
+ * of all the files in the command line, one by one *)
+
+let files = ref []
+
+let parse_cl () =
+ Arg.parse
+ [ "-o", Arg.String (fun s -> output_specified := true; output := s),
+ "output-file Specifiy the resulting LaTeX file";
+ "-n", Arg.Int (fun n -> linelen := n),
+ "line-width Set the line width";
+ "-image", Arg.String (fun s -> image := s),
+ "coq-image Use coq-image as Coq command";
+ "-w", Arg.Set cut_at_blanks,
+ " Try to cut lines at blanks";
+ "-v", Arg.Set verbose,
+ " Verbose mode (show Coq answers on stdout)";
+ "-sl", Arg.Set slanted,
+ " Coq answers in slanted font (only with LaTeX2e)";
+ "-hrule", Arg.Set hrule,
+ " Coq parts are written between 2 horizontal lines";
+ "-small", Arg.Set small,
+ " Coq parts are written in small font";
+ "-boot", Arg.Set boot,
+ " Launch coqtop with the -boot option"
+ ]
+ (fun s -> files := s :: !files)
+ "coq-tex [options] file ..."
+
+let find_coqtop () =
+ let prog = Sys.executable_name in
+ try
+ let size = String.length prog in
+ let i = Str.search_backward (Str.regexp_string "coq-tex") prog (size-7) in
+ (String.sub prog 0 i)^"coqtop"^(String.sub prog (i+7) (size-i-7))
+ with Not_found -> begin
+ Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
+ "coqtop"
+ end
+
+let main () =
+ parse_cl ();
+ if !image = "" then image := Filename.quote (find_coqtop ());
+ if !boot then image := !image ^ " -boot";
+ if Sys.command (!image ^ " -batch -silent") <> 0 then begin
+ Printf.printf "Error: ";
+ let _ = Sys.command (!image ^ " -batch") in
+ exit 1
+ end else begin
+ Printf.printf "Your version of coqtop seems OK\n";
+ flush stdout
+ end;
+ List.iter one_file (List.rev !files)
+
+let _ = Printexc.catch main ()