matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml

   1 module ET = MrcTypes
   2
   3 let read_substs substs ich =
   4   let map subst =
   5     let words = String.split_on_char ' ' subst in
   6     List.filter ((<>) "") words
   7   in
   8   while true do
   9     let line = input_line ich in
  10     let subst = String.split_on_char ',' line in
  11     substs := List.map map subst :: !substs
  12   done
  13
  14 let read_file file =
  15   let ich = open_in file in
  16   let line = input_line ich in
  17   let scan r f d p o = r, f, d, p, o in
  18   let rmod, rfun, dmod, para, optn =
  19     Scanf.sscanf line "%s %s %S %b %b" scan
  20   in
  21   let substs = ref [] in
  22   begin
  23     try read_substs substs ich with
  24     | End_of_file -> close_in ich
  25   end;
  26   {
  27      ET.cmod = Filename.remove_extension file;
  28      rmod; rfun; dmod; para; optn;
  29      substs = !substs;
  30   }
  31
  32 let list_rev_filter_map filter map l =
  33   let rec aux r = function
  34     | []       -> r
  35     | hd :: tl -> if filter hd then aux (map hd :: r) tl else aux r tl
  36   in
  37   aux [] l
  38
  39 let read_dir file =
  40   let filter name =
  41     Filename.extension name = ".mrc"
  42   in
  43   let map name =
  44     Filename.remove_extension name
  45   in
  46   let dir = Array.to_list (Sys.readdir file) in
  47   let mods = List.fast_sort Pervasives.compare (list_rev_filter_map filter map dir) in
  48   {
  49     ET.cdir = file; mods;
  50   }
  51
  52 let rec read_mods mods ich =
  53   let line = input_line ich in
  54   let scan _ m =
  55     mods := m :: !mods
  56   in
  57   Scanf.sscanf line "module %s = RecommGc%s" scan;
  58   read_mods mods ich
  59
  60 let read_index dir =
  61   let file = Filename.concat dir "recommGc.ml" in
  62   let mods = ref [] in
  63   if Sys.file_exists file then begin
  64     let ich = open_in file in
  65     try read_mods mods ich with
  66     | End_of_file -> close_in ich
  67   end;
  68   let mods = List.fast_sort Pervasives.compare !mods in
  69   {
  70     ET.cdir = dir; mods;
  71   }