X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fbin%2Finline%2Finline.ml;fp=helm%2Fwww%2Flambdadelta%2Fbin%2Finline%2Finline.ml;h=905f7ec4d3d2137d0af1756fa5c13f7d7f86cf04;hb=d8d00d6f6694155be5be486a8239f5953efe28b7;hp=0000000000000000000000000000000000000000;hpb=3f57ed2589601e79478c85d74708d8ebdec2cf20;p=helm.git

diff --git a/helm/www/lambdadelta/bin/inline/inline.ml b/helm/www/lambdadelta/bin/inline/inline.ml
new file mode 100644
index 000000000..905f7ec4d
--- /dev/null
+++ b/helm/www/lambdadelta/bin/inline/inline.ml
@@ -0,0 +1,162 @@
+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 ()