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

   1 module ET = MrcTypes
   2
   3 let cap = String.capitalize_ascii
   4
   5 let ko b =
   6   if b then "KO" else "OO"
   7
   8 let write_mli name =
   9   let file = name ^ ".mli" in
  10   if Sys.file_exists file then ()
  11   else begin
  12     let och = open_out file in
  13     close_out och
  14   end
  15
  16 let write_subst st och subst =
  17   let iter hd words =
  18     let lhs = List.map (Printf.sprintf "%S :: ") words in
  19     let rhs = List.map (Printf.sprintf "%S :: ") hd in
  20     Printf.fprintf och "  | %stl -> k T.OK (%souts) tl\n"
  21       (String.concat "" lhs) (String.concat "" rhs)
  22   in
  23   match subst with
  24   | []      -> ()
  25   | hd :: _ -> List.iter (iter (List.rev hd)) subst
  26
  27 let write_component st =
  28   let cmod = "recommGc" ^ st.ET.cmod in
  29   let och = open_out (cmod ^ ".ml") in
  30   Printf.fprintf och "module T = RecommTypes\n";
  31   Printf.fprintf och "module R = Recomm%s\n" (cap st.ET.rmod);
  32   if st.ET.dmod <> "" then begin
  33     Printf.fprintf och "module D = Recomm%s\n" (cap st.ET.dmod)
  34   end;
  35   Printf.fprintf och "\n";
  36   Printf.fprintf och "let step k st outs ins =\n";
  37   if st.ET.para then begin
  38     Printf.fprintf och "  if st <> T.OO then k st outs ins else\n"
  39   end else begin
  40     Printf.fprintf och "  if st = T.KO then k st outs ins else\n"
  41   end;
  42   Printf.fprintf och "  match ins with\n";
  43   List.iter (write_subst st och) st.ET.substs;
  44   Printf.fprintf och "  | _ -> k T.%s outs ins\n\n" (ko st.ET.optn);
  45   Printf.fprintf och "let main =\n";
  46   Printf.fprintf och "  R.register_%s step\n" st.ET.rfun;
  47   close_out och;
  48   write_mli cmod
  49
  50 let write_index st =
  51   let cmod = Filename.concat st.ET.cdir "recommGc" in
  52   let och = open_out (cmod ^ ".ml") in
  53   let iter i name =
  54     Printf.fprintf och "module G%03u = RecommGc%s\n" (succ i) name
  55   in
  56   List.iteri iter st.ET.mods;
  57   close_out och;
  58   write_mli cmod