matita/matita/contribs/lambdadelta/bin/inline/inline.ml

   1 module Deps  = Set.Make(String)
   2 module Table = Map.Make(String)
   3
   4 let opt_map f = function
   5   | None   -> None
   6   | Some a -> Some (f a)
   7
   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
  11
  12 let filename_concat l =
  13   String.concat Filename.dir_sep l
  14
  15 let relative s =
  16   match filename_split [] s with
  17   | "cic:" :: "matita" :: "lambdadelta" :: tl -> List.rev tl
  18   | _                                         -> []
  19
  20 let to_string l =
  21   filename_concat (List.rev l)
  22
  23 let table = ref (Table.empty: Deps.t Table.t)
  24
  25 let add src dep =
  26   let deps = match Table.find_opt src !table with
  27   | None      -> Deps.singleton dep
  28   | Some deps -> Deps.add dep deps
  29   in
  30   table := Table.add src deps !table
  31
  32 let split_or s =
  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 -> ""
  36
  37 let split_and s =
  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 -> ""
  41
  42 let split_ex s =
  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 -> ""
  46
  47 let split_ex1 s =
  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 -> ""
  51
  52 let map_deps s1 s2 =
  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
  60     let r2 =
  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)
  70     in
  71     if r1 <> "ground_2/xoa/xoa" then add r1 r2
  72   | _                           -> ()
  73
  74 let reds = ref []
  75
  76 let map_reds s1 s2 =
  77   reds := (s1,s2) :: !reds
  78
  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
  86     end
  87   end;
  88   read map_deps map_reds ich
  89
  90 let xoadir = ref "ground_2/xoa"
  91
  92 let print_deps () =
  93   let map_d src dep =
  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
  98   in
  99   let map_t src deps =
 100     Deps.iter (map_d src) deps
 101   in
 102   Table.iter map_t !table
 103
 104 let rec copy xn ich och =
 105   if xn = Some 0 then ()
 106   else begin
 107     Printf.fprintf och "%s\n" (input_line ich);
 108     copy (opt_map pred xn) ich och
 109   end
 110
 111 let base_dir = ref ""
 112
 113 let preamble = ref 14
 114
 115 let insert_deps () =
 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
 119   in
 120   let map_r och rdep =
 121     Printf.fprintf och "include %S.\n" rdep;
 122   in
 123   let map_t src deps =
 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
 129       Sys.rename ma old;
 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
 136     end
 137   in
 138   Table.iter map_t !table
 139
 140 let process fname =
 141   let ich = open_in fname in
 142   try read map_deps map_reds ich with
 143   | End_of_file -> close_in ich
 144
 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> ]*"
 150
 151 let print = ref false
 152 let insert = ref false
 153
 154 let _ =
 155   Arg.parse [
 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;
 160   ] process help;
 161   if !print then print_deps ();
 162   if !insert then insert_deps ()