2 module ET = RecommTypes
6 let replace = ref false
8 let string_length_utf8 s =
9 let l = String.length s in
12 if '\x80' <= s.[i] && s.[i] <= '\xBF'
13 then aux (succ r) (succ i) else aux r (succ i)
18 let l = !width - string_length_utf8 s - 5 - n in
20 Printf.eprintf "overfull: %S\n" s;
26 let out_src och = function
28 Printf.fprintf och "%s" s
30 Printf.fprintf och "%s" s
32 Printf.fprintf och "(* *%s*)" s
35 if s1 = "NOTE" then complete (s1^s2) 0 else ""
37 Printf.fprintf och "(* %s%s%s*)" s1 s2 s3
39 let s = String.concat " " ss in
40 Printf.fprintf och "(* %s %s*)" s (complete s 1)
42 let s = String.capitalize_ascii (String.concat " " ss) in
43 Printf.fprintf och "(* %s %s*)" s (complete s 1)
44 | ET.Other (_, s1, s2, s3) ->
45 Printf.fprintf och "%s%s%s" s1 s2 s3
47 let write_srcs file srcs =
49 if !replace then begin
50 Sys.rename file (file ^ ".old");
56 let och = open_out target in
57 List.iter (out_src och) srcs;
60 let write_subst och n s =
61 Printf.fprintf och "%s %s\n" s n
63 let rec write_fst och = function
65 | ET.Other (2, _, s, _) :: ET.Line _ :: ET.Text t :: tl ->
66 write_snd och tl s (EL.split_on_char ' ' t)
67 | ET.Other (2, _, s, _) :: tl ->
68 Printf.eprintf "skipping fst: %S\n" s;
70 | _ :: tl -> write_fst och tl
72 and write_snd och tl s = function
74 | "definition" :: n :: _
75 | "corec" :: "definition" :: n :: _
76 | "rec" :: "definition" :: n :: _
78 | "corec" :: "fact" :: n :: _
80 | "corec" :: "lemma" :: n :: _
82 | "corec" :: "theorem" :: n :: _
83 | "inductive" :: n :: _
84 | "coinductive" :: n :: _
86 let ss = EL.split_on_char ' ' s in
87 List.iter (write_subst och n) (List.tl ss);
90 Printf.eprintf "skipping snd: %S %S\n" s t;
93 Printf.eprintf "skipping snd: %S\n" s;
96 let write_substs = write_fst