aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_tex.ml
blob: 7bc547c684266f13ddf0346aa1f106dacbe606ee (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \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 any_prompt = Str.regexp "[A-Z0-9a-z_\\$']* < "

(* 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 ->
    (* a dummy command, just in case the last line was a comment *)
    output_string chan_out "Set Printing Width 78.\n";
    close_in chan_in;
    close_out chan_out

(* Second pass: insert the answers of Coq from [coq_output] into the
 * TeX file [texfile]. The result goes in file [result]. *)

let tex_escaped s =
  let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in
  let adapt_delim = function
    | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
    | "_" -> "{\\char`\\_}"
    | "\\" -> "{\\char'134}"
    | "^" -> "{\\char'136}"
    | "~" -> "{\\char'176}"
    | " " -> "~"
    | "<" -> "{<}"
    | ">" -> "{>}"
    | "'" -> "{\\textquotesingle}"
    | "`" -> "\\`{}"
    | _ -> 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
  (* read lines until a prompt is found (starting from the second line),
     purge prompts on the first line and return their number *)
  let last_read = ref (input_line c_coq) in
  let read_output () =
    let first = !last_read in
    let nb = ref 0 in
    (* remove the leading prompts *)
    let rec skip_prompts pos =
      if Str.string_match any_prompt first pos then
        let () = incr nb in
        skip_prompts (Str.match_end ())
      else pos in
    let first =
      let start = skip_prompts 0 in
      String.sub first start (String.length first - start) in
    (* 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
    (first :: read_lines (), !nb) in
  let unhandled_output = ref None in
  let read_output () =
    match !unhandled_output with
    | Some some -> unhandled_output := None; some
    | None -> read_output () in
  (* we are inside a \begin{coq_...} ... \end{coq_...} block
   * show_... tell what kind of block it is *)
  let rec inside show_answers show_questions not_first discarded =
    let s = input_line c_tex in
    if s = "" then
      inside show_answers show_questions not_first (discarded + 1)
    else if not (Str.string_match end_coq s 0) then begin
      let (bl,n) = read_output () in
      assert (n > discarded);
      let n = n - discarded in
      if not_first then output_string c_out "\\medskip\n";
      if !verbose then Printf.printf "Coq < %s\n" s;
      if show_questions then encapsule false c_out ("Coq < " ^ s);
      let rec read_lines k =
        if k = 0 then []
        else
          let s = input_line c_tex in
          if Str.string_match end_coq s 0 then []
          else s :: read_lines (k - 1) in
      let al = read_lines (n - 1) in
      if !verbose then List.iter (Printf.printf "      %s\n") al;
      if show_questions then
        List.iter (fun s -> encapsule false c_out ("      " ^ s)) al;
      let la = n - 1 - List.length al in
      if la <> 0 then
        (* this happens when the block ends with a comment; the output
           is for the command at the beginning of the next block *)
        unhandled_output := Some (bl, la)
      else begin
        if !verbose then List.iter print_endline bl;
        if show_answers then print_block c_out bl;
        inside show_answers show_questions (show_answers || show_questions) 0
      end
    end else if discarded > 0 then begin
      (* this happens when the block ends with an empty line *)
      let (bl,n) = read_output () in
      assert (n > discarded);
      unhandled_output := Some (bl, n - discarded)
    end in
  (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
  let rec outside just_after =
    let start_block () =
      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" in
    let end_block () =
      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" in
    let s = input_line c_tex in
    if Str.string_match begin_coq s 0 then begin
      let kind = Str.matched_group 1 s in
      if kind = "eval" then begin
        if just_after then end_block ();
        inside false false false 0;
        outside false
      end else begin
        let show_answers   = kind <> "example*" in
        let show_questions = kind <> "example#" in
        if not just_after then start_block ();
        inside show_answers show_questions just_after 0;
        outside true
      end
    end else begin
      if just_after then end_block ();
      output_string c_out (s ^ "\n");
      outside false
    end in
  try
    let _ = read_output () in (* to skip the Coq banner *)
    let _ = read_output () in (* to skip the Coq answer to Set Printing Width *)
    outside false
  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 reraise -> begin
    rm inputv; rm coq_output;
    raise reraise
  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    Specify 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 _ =
  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)