(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: coq-tex.ml4 9532 2007-01-24 16:04:29Z bgregoir $ *)
(* 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 _ =
match Sys.os_type with
| "Unix" -> ()
| _ -> begin
print_string "This program only runs under Unix !\n";
flush stdout;
exit 1
end
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 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 rec trans = parser
| [< s1 = (parser
| [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] ->
"\\" ^ (String.make 1 c)
| [< ''\\' >] -> "{\\char'134}"
| [< ''^' >] -> "{\\char'136}"
| [< ''~' >] -> "{\\char'176}"
| [< '' ' >] -> "~"
| [< ''<' >] -> "{<}"
| [< ''>' >] -> "{>}"
| [< 'c >] -> String.make 1 c);
s2 = trans >] -> s1 ^ s2
| [< >] -> ""
in
trans (Stream.of_string 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"
]
(fun s -> files := s :: !files)
"coq-tex [options] file ..."
let main () =
parse_cl ();
if !image = "" then begin
Printf.printf "Warning: preprocessing with default image \"coqtop\"\n";
image := "coqtop"
end;
if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 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 ()