--- /dev/null
+module Deps = Set.Make(String)
+module Table = Map.Make(String)
+
+let opt_map f = function
+ | None -> None
+ | Some a -> Some (f a)
+
+let rec filename_split l s =
+ let dir, base = Filename.dirname s, Filename.basename s in
+ if dir = Filename.current_dir_name then base::l else filename_split (base::l) dir
+
+let filename_concat l =
+ String.concat Filename.dir_sep l
+
+let relative s =
+ match filename_split [] s with
+ | "cic:" :: "matita" :: "lambdadelta" :: tl -> List.rev tl
+ | _ -> []
+
+let to_string l =
+ filename_concat (List.rev l)
+
+let table = ref (Table.empty: Deps.t Table.t)
+
+let add src dep =
+ let deps = match Table.find_opt src !table with
+ | None -> Deps.singleton dep
+ | Some deps -> Deps.add dep deps
+ in
+ table := Table.add src deps !table
+
+let split_or s =
+ let map m = Printf.sprintf "or_%u" m in
+ try Scanf.sscanf s "or%u" map
+ with Scanf.Scan_failure _ | End_of_file -> ""
+
+let split_and s =
+ let map m = Printf.sprintf "and_%u" m in
+ try Scanf.sscanf s "and%u" map
+ with Scanf.Scan_failure _ | End_of_file -> ""
+
+let split_ex s =
+ let map m n = Printf.sprintf "ex_%u_%u" m n in
+ try Scanf.sscanf s "ex%u=%u" map
+ with Scanf.Scan_failure _ | End_of_file -> ""
+
+let split_ex1 s =
+ let map m = Printf.sprintf "ex_%u_1" m in
+ try Scanf.sscanf s "ex%u" map
+ with Scanf.Scan_failure _ | End_of_file -> ""
+
+let map_deps s1 s2 =
+ match relative s2 with
+ | [b2;"xoa";"xoa";"ground_2"] ->
+ let r1 = List.tl (relative s1) in
+ let r1 = to_string r1 in
+ let b2 = Filename.remove_extension b2 in
+(* '_' is accepted (and ignored) within integer literals *)
+ let b2 = String.concat "=" (String.split_on_char '_' b2) in
+ let r2 =
+ let cx = split_ex b2 in
+ let cy = split_ex1 b2 in
+ let ca = split_and b2 in
+ let co = split_or b2 in
+ if cx <> "" then cx else
+ if cy <> "" then cy else
+ if ca <> "" then ca else
+ if co <> "" then co else
+ failwith (Printf.sprintf "unrecognized xoa: %S\n" b2)
+ in
+ if r1 <> "ground_2/xoa/xoa" then add r1 r2
+ | _ -> ()
+
+let reds = ref []
+
+let map_reds s1 s2 =
+ reds := (s1,s2) :: !reds
+
+let rec read map_deps map_reds ich =
+ let line = input_line ich in
+ begin try Scanf.sscanf line "%S: %S" map_deps
+ with Scanf.Scan_failure _ | End_of_file ->
+ begin try Scanf.sscanf line "%S: redundant %S" map_reds
+ with Scanf.Scan_failure _ | End_of_file ->
+ Printf.eprintf "unknown line: %s.\n" line
+ end
+ end;
+ read map_deps map_reds ich
+
+let xoadir = ref "ground_2/xoa"
+
+let print_deps () =
+ let map_d src dep =
+ let src = src^".ma" in
+ let dep = Filename.concat !xoadir (dep^".ma") in
+ if List.mem (src,dep) !reds then ()
+ else Printf.printf "%S: %S\n" src dep
+ in
+ let map_t src deps =
+ Deps.iter (map_d src) deps
+ in
+ Table.iter map_t !table
+
+let rec copy xn ich och =
+ if xn = Some 0 then ()
+ else begin
+ Printf.fprintf och "%s\n" (input_line ich);
+ copy (opt_map pred xn) ich och
+ end
+
+let base_dir = ref ""
+
+let preamble = ref 14
+
+let insert_deps () =
+ let map_d src dep rdeps =
+ let dep = Filename.concat !xoadir (dep^".ma") in
+ if List.mem (src,dep) !reds then rdeps else dep::rdeps
+ in
+ let map_r och rdep =
+ Printf.fprintf och "include %S.\n" rdep;
+ in
+ let map_t src deps =
+ let src = src^".ma" in
+ let rdeps = Deps.fold (map_d src) deps [] in
+ if rdeps <> [] then begin
+ let ma = Filename.concat !base_dir src in
+ let old = ma^".old" in
+ Sys.rename ma old;
+ let och = open_out ma in
+ let ich = open_in old in
+ copy (Some !preamble) ich och;
+ List.iter (map_r och) (List.rev rdeps);
+ try copy None ich och
+ with End_of_file -> close_in ich; close_out och
+ end
+ in
+ Table.iter map_t !table
+
+let process fname =
+ let ich = open_in fname in
+ try read map_deps map_reds ich with
+ | End_of_file -> close_in ich
+
+let help_b = "<dir> Set this base directory (default: current directory)"
+let help_i = " Insert the dependences (default: no)"
+let help_l = "<int> .ma preamble has theese lines (default: 14)"
+let help_p = " Print the dependences to be inserted (default: no)"
+let help = "inline [ -ip | -b <dir> | -l <int> | <file> ]*"
+
+let print = ref false
+let insert = ref false
+
+let _ =
+ Arg.parse [
+ "-b", Arg.String ((:=) base_dir), help_b;
+ "-l", Arg.Int ((:=) preamble), help_l;
+ "-i", Arg.Set insert, help_i;
+ "-p", Arg.Set print, help_p;
+ ] process help;
+ if !print then print_deps ();
+ if !insert then insert_deps ()
projects / helm.git / blobdiff