From b6a043c3ed2eec9fb36e22426b856d689d96a939 Mon Sep 17 00:00:00 2001
From: Ryota Kobayashi <ryota5884@icloud.com>
Date: Mon, 6 Nov 2023 18:01:35 +0900
Subject: [PATCH] run mochi automatically (may error occurs)

---
 .gitignore       | 1 +
 src/callMoCHi.ml | 8 +++++---
 src/consort.ml   | 8 +++++++-
 src/convMoCHi.ml | 4 ++++
 4 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/.gitignore b/.gitignore
index 05c41159..4a1cca45 100644
--- a/.gitignore
+++ b/.gitignore
@@ -27,3 +27,4 @@ paper/related_work.tex
 paper/semantics.tex
 paper/typesystem.tex
 paper/wf_rules.tex
+src/test/to_mochi.ml
diff --git a/src/callMoCHi.ml b/src/callMoCHi.ml
index e465e4fd..57a9a00e 100644
--- a/src/callMoCHi.ml
+++ b/src/callMoCHi.ml
@@ -1,4 +1,6 @@
 let call_mochi =
-  let cmd = "~/git/MoCHi/src.mochi.exe ./test/to_mochi.ml" in
-  let proc = Process.spawn cmd in
-  
\ No newline at end of file
+  let cmd = "~/git/MoCHi/src/mochi.exe ./test/to_mochi.ml" in
+  let p = Process.spawn cmd in
+  let res = (String.trim @@ input_line p.Process.proc_stdout, String.trim @@ input_line p.Process.proc_stderr) in
+  Process.dispose p;
+  res
\ No newline at end of file
diff --git a/src/consort.ml b/src/consort.ml
index 28c8b5ca..f7152143 100644
--- a/src/consort.ml
+++ b/src/consort.ml
@@ -242,5 +242,11 @@ let convmochi ~opts file =
       ((function Some x -> x | None -> assert false) ownership_res)
       ast
   in
-  ConvMoCHi.Mochi.print_prog prog;
+  (* ConvMoCHi.Mochi.print_prog prog; *)
+  let file = open_out "./test/to_mochi.ml" in
+  ConvMoCHi.Mochi.write_to_channel_prog prog file;
+  Out_channel.close file;
+  let (res_out, res_err) = CallMoCHi.call_mochi in
+  print_endline res_out;
+  print_endline res_err;
   match ownership_res with None -> Unverified Aliasing | Some _ -> Verified
diff --git a/src/convMoCHi.ml b/src/convMoCHi.ml
index e970d8f0..cef56f90 100644
--- a/src/convMoCHi.ml
+++ b/src/convMoCHi.ml
@@ -265,6 +265,10 @@ module Mochi = struct
   let print_prog prog =
     print_endline builtin;
     pp_prog prog std_formatter
+
+  let write_to_channel_prog prog file =
+    Printf.fprintf file "%s\n" builtin;
+    pp_prog prog (Format.formatter_of_out_channel file);
 end
 
 let pull_type ty con i =