summaryrefslogtreecommitdiff
path: root/tools/coq_tex.ml4
blob: 485162eee8b080784c1868f99efb376cfe4aa475 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \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 _ =
  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 ()