blob: f050f7537671c4b68ca8315498beb859bd5f7fb4 (
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
|
open Printf
let file = Sys.argv.(1)
let cin = open_in file
let cout = open_out (file ^ ".v8")
let (coq_out, coq_in) as chan = Unix.open_process "coqtop -translate"
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 new_syntax =
Str.regexp "New Syntax:[ \t]*$"
(* on envoie un Check O et on saute les 2 premiers New Syntax *)
let _ =
output_string coq_in "Check O.\n";
flush coq_in;
while not (Str.string_match new_syntax (input_line coq_out) 0) do () done;
while not (Str.string_match new_syntax (input_line coq_out) 0) do () done;
printf "** init terminée\n"; flush stdout
let iter_char_until_dot cin f =
printf "** entrée dans iter_char\n"; flush stdout;
let last_c = ref ' ' in
let rec loop () =
let c = input_char cin in
printf "[%c]" c; flush stdout;
f c;
if !last_c = '.' && (c = ' ' || c = '\t' || c = '\n') then
()
else begin
last_c := c;
loop ()
end
in
loop ()
let trad_commands () =
(* on copie toutes les commandes dans un fichier temporaire *)
let tmp = Filename.temp_file "trad" ".v" in
let tmp_in, end_s =
let tmp_out = open_out tmp in
let rec loop () =
let s = input_line cin in
if Str.string_match end_coq s 0 then begin
close_out tmp_out;
open_in tmp, s
end else begin
output_string tmp_out (s ^ "\n");
loop ()
end
in
loop ()
in
ignore (Sys.command (Printf.sprintf "cat %s" tmp));
let one_command () =
(* on envoie toute la commande a Coq *)
iter_char_until_dot tmp_in (fun c -> output_char coq_in c);
(* on flush *)
flush coq_in;
(* on lit la réponse *)
try
(* 1. on cherche la ligne "New Syntax:" *)
while true do
let s = input_line coq_out in
if Str.string_match new_syntax s 0 then raise Exit
done
with Exit ->
(* 2. on copie tout jusqu'au point *)
printf "** New Syntax trouvé\n"; flush stdout;
iter_char_until_dot coq_out (fun c -> output_char cout c);
printf "** copie terminée\n"; flush stdout;
flush cout
in
try
while true do one_command () done; assert false
with End_of_file ->
printf "** End_of_file\n"; flush stdout;
Sys.remove tmp;
end_s
let trad () =
while true do
let s = input_line cin in
output_string cout (s ^ "\n");
if Str.string_match begin_coq s 0 then
let s = trad_commands () in
output_string cout (s ^ "\n");
done
let _ =
try
trad ()
with End_of_file ->
close_out cout;
printf "** close_out cout\n"; flush stdout;
ignore (Unix.close_process chan)
|
