From 5c9019003187f14797ba4d4514fec1cf2ac03d65 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Feb 2022 02:00:54 +0100
Subject: Make minor modifications with regards to unit tests

---
 Makefile              | 2 +-
 src/ExtractToFStar.ml | 7 ++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 93ac5b2e..e17d4197 100644
--- a/Makefile
+++ b/Makefile
@@ -19,7 +19,7 @@ build:
 .PHONY: build-run
 build-run: build
 	dune exec -- src/main.exe $(CFIM_TEST_FILE1) -dest $(DEST_DIR) -test-units -test-trans-units > tests/trace_current.txt
-	dune exec -- src/main.exe $(CFIM_TEST_FILE2) -dest $(DEST_DIR)
+	dune exec -- src/main.exe $(CFIM_TEST_FILE2) -dest $(DEST_DIR) -test-trans-units
 
 # Build the project and run the executable, then check that the behaviour
 # of the interpreter didn't change by comparing the newly generated trace
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 5bf33677..0c77f48b 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1026,7 +1026,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
   let sg = def.signature in
   if
     sg.type_params = []
-    && sg.inputs = [ unit_ty ]
+    && (sg.inputs = [ unit_ty ] || sg.inputs = [])
     && sg.outputs = [ mk_result_ty unit_ty ]
   then (
     (* Add a break before *)
@@ -1045,8 +1045,9 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_string fmt "(";
     let fun_name = ctx_get_local_function def.def_id def.back_id ctx in
     F.pp_print_string fmt fun_name;
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "()";
+    if sg.inputs <> [] then (
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "()");
     F.pp_print_space fmt ();
     F.pp_print_string fmt "=";
     F.pp_print_space fmt ();
-- 
cgit v1.2.3