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

   1 module ET = MrcTypes
   2
   3 let cap = String.capitalize_ascii
   4
   5 let ok b =
   6   if b then "true" else "ok"
   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 %s (%souts) tl\n"
  21       (String.concat "" lhs) (ok st.ET.para) (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   if st.ET.dmod <> "" then begin
  31     Printf.fprintf och "module D = Recomm%s\n\n" (cap st.ET.dmod)
  32   end;
  33   Printf.fprintf och "let step k ok outs ins =\n";
  34   Printf.fprintf och "  if ok then k ok outs ins else\n";
  35   Printf.fprintf och "  match ins with\n";
  36   List.iter (write_subst st och) st.ET.substs;
  37   Printf.fprintf och "  | _ -> k %s outs ins\n\n" (ok st.ET.optn);
  38   Printf.fprintf och "let main =\n";
  39   Printf.fprintf och "  Recomm%s.register_%s step\n" (cap st.ET.rmod) st.ET.rfun;
  40   close_out och;
  41   write_mli cmod
  42
  43 let write_index st =
  44   let cmod = Filename.concat st.ET.cdir "recommGc" in
  45   let och = open_out (cmod ^ ".ml") in
  46   let iter i name =
  47     Printf.fprintf och "module G%u = RecommGc%s\n" (succ i) name
  48   in
  49   List.iteri iter st.ET.mods;
  50   close_out och;
  51   write_mli cmod