Merge pull request #41 from SoftwareFoundationGroupAtKyotoU/feature/c…

…all-mochi [WIP] Call MoCHi automatically
SoftwareFoundationGroupAtKyotoU · Mar 21, 2024 · b17ea89 · b17ea89
2 parents c44a49a + 088f7ee
commit b17ea89
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 2 deletions.
diff --git a/src/callMoCHi.ml b/src/callMoCHi.ml
diff --git a/src/consort.ml b/src/consort.ml
@@ -242,5 +242,8 @@ 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;
   match ownership_res with None -> Unverified Aliasing | Some _ -> Verified
diff --git 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 =

diff --git a/src/test/list/reverse2.imp b/src/test/list/reverse2.imp
@@ -10,6 +10,7 @@ mklist(n) {
 _reverse(l, l_next) {
     match l_next with
       Nil -> {
+        // FIXME: this alias statement is (maybe) wrong
         // alias(*(l.Cons.2) = l_next);
         return l
       }
@@ -51,4 +52,4 @@ len(l) {
     let len_l = len(l) in
     let rev_l = reverse(l) in
     assert(len_l = len(rev_l))
-}
+}