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

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