1 module Deps = Set.Make(String)
2 module Table = Map.Make(String)
4 let opt_map f = function
8 let rec filename_split l s =
9 let dir, base = Filename.dirname s, Filename.basename s in
10 if dir = Filename.current_dir_name then base::l else filename_split (base::l) dir
12 let filename_concat l =
13 String.concat Filename.dir_sep l
16 match filename_split [] s with
17 | "cic:" :: "matita" :: "lambdadelta" :: tl -> List.rev tl
21 filename_concat (List.rev l)
23 let table = ref (Table.empty: Deps.t Table.t)
26 let deps = match Table.find_opt src !table with
27 | None -> Deps.singleton dep
28 | Some deps -> Deps.add dep deps
30 table := Table.add src deps !table
33 let map m = Printf.sprintf "or_%u" m in
34 try Scanf.sscanf s "or%u" map
35 with Scanf.Scan_failure _ | End_of_file -> ""
38 let map m = Printf.sprintf "and_%u" m in
39 try Scanf.sscanf s "and%u" map
40 with Scanf.Scan_failure _ | End_of_file -> ""
43 let map m n = Printf.sprintf "ex_%u_%u" m n in
44 try Scanf.sscanf s "ex%u=%u" map
45 with Scanf.Scan_failure _ | End_of_file -> ""
48 let map m = Printf.sprintf "ex_%u_1" m in
49 try Scanf.sscanf s "ex%u" map
50 with Scanf.Scan_failure _ | End_of_file -> ""
53 match relative s2 with
54 | [b2;"xoa";"xoa";"ground_2"] ->
55 let r1 = List.tl (relative s1) in
56 let r1 = to_string r1 in
57 let b2 = Filename.remove_extension b2 in
58 (* '_' is accepted (and ignored) within integer literals *)
59 let b2 = String.concat "=" (String.split_on_char '_' b2) in
61 let cx = split_ex b2 in
62 let cy = split_ex1 b2 in
63 let ca = split_and b2 in
64 let co = split_or b2 in
65 if cx <> "" then cx else
66 if cy <> "" then cy else
67 if ca <> "" then ca else
68 if co <> "" then co else
69 failwith (Printf.sprintf "unrecognized xoa: %S\n" b2)
71 if r1 <> "ground_2/xoa/xoa" then add r1 r2
77 reds := (s1,s2) :: !reds
79 let rec read map_deps map_reds ich =
80 let line = input_line ich in
81 begin try Scanf.sscanf line "%S: %S" map_deps
82 with Scanf.Scan_failure _ | End_of_file ->
83 begin try Scanf.sscanf line "%S: redundant %S" map_reds
84 with Scanf.Scan_failure _ | End_of_file ->
85 Printf.eprintf "unknown line: %s.\n" line
88 read map_deps map_reds ich
90 let xoadir = ref "ground_2/xoa"
94 let src = src^".ma" in
95 let dep = Filename.concat !xoadir (dep^".ma") in
96 if List.mem (src,dep) !reds then ()
97 else Printf.printf "%S: %S\n" src dep
100 Deps.iter (map_d src) deps
102 Table.iter map_t !table
104 let rec copy xn ich och =
105 if xn = Some 0 then ()
107 Printf.fprintf och "%s\n" (input_line ich);
108 copy (opt_map pred xn) ich och
111 let base_dir = ref ""
113 let preamble = ref 14
116 let map_d src dep rdeps =
117 let dep = Filename.concat !xoadir (dep^".ma") in
118 if List.mem (src,dep) !reds then rdeps else dep::rdeps
121 Printf.fprintf och "include %S.\n" rdep;
124 let src = src^".ma" in
125 let rdeps = Deps.fold (map_d src) deps [] in
126 if rdeps <> [] then begin
127 let ma = Filename.concat !base_dir src in
128 let old = ma^".old" in
130 let och = open_out ma in
131 let ich = open_in old in
132 copy (Some !preamble) ich och;
133 List.iter (map_r och) (List.rev rdeps);
134 try copy None ich och
135 with End_of_file -> close_in ich; close_out och
138 Table.iter map_t !table
141 let ich = open_in fname in
142 try read map_deps map_reds ich with
143 | End_of_file -> close_in ich
145 let help_b = "<dir> Set this base directory (default: current directory)"
146 let help_i = " Insert the dependences (default: no)"
147 let help_l = "<int> .ma preamble has theese lines (default: 14)"
148 let help_p = " Print the dependences to be inserted (default: no)"
149 let help = "inline [ -ip | -b <dir> | -l <int> | <file> ]*"
151 let print = ref false
152 let insert = ref false
156 "-b", Arg.String ((:=) base_dir), help_b;
157 "-l", Arg.Int ((:=) preamble), help_l;
158 "-i", Arg.Set insert, help_i;
159 "-p", Arg.Set print, help_p;
161 if !print then print_deps ();
162 if !insert then insert_deps ()