create output file

minuska/bin/dune

@@ -12,5 +12,6 @@
  (public_name minuska)
  (name main)
  (modules syntax parser lexer main)
- (libraries core core_unix.command_unix)
+ (libraries core core_unix.command_unix core_unix.filename_unix)
+ (preprocess (pps ppx_jane))
  )

minuska/bin/main.ml

@@ -28,17 +28,26 @@ let parse_and_print lexbuf =
     print_definition value
   | None -> ()
 
-let loop filename () =
-  let inx = In_channel.create filename in
+let transform input_filename output_filename () =
+  let inx = In_channel.create input_filename in
+  let oux = Out_channel.create output_filename in
   let lexbuf = Lexing.from_channel inx in
-  lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
+  lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = input_filename };
   parse_and_print lexbuf;
+  Out_channel.close oux;
   In_channel.close inx
 
-let () =
-  print_endline "Hello, World (1)!";
-  Command.basic_spec ~summary:"Parse and display a language definition"
-    Command.Spec.(empty +> anon ("filename" %: string))
-    loop
-  |> Command_unix.run
+
+let command =
+  Command.basic
+    ~summary:"Generate a Coq (*.v) file from a Minuska (*.m) file"
+    ~readme:(fun () -> "TODO")
+    (let%map_open.Command
+        input_filename = anon (("filename_in" %: Filename_unix.arg_type)) and
+        output_filename = anon (("filename_out" %: Filename_unix.arg_type))
+
+     in
+     fun () -> transform input_filename output_filename ())
+
+let () = Command_unix.run ~version:"1.0" ~build_info:"RWO" command