From 72edb3fc4fdfa588d0cebe7fec27101da27ff1be Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Feb 2022 23:12:39 +0100
Subject: Fix a small issue with the unit type

---
 src/ExtractToFStar.ml  | 13 +++++++++----
 src/PureMicroPasses.ml |  4 +++-
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 3ca003a4..d1e1176c 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -37,6 +37,7 @@ let fstar_keywords =
     "with";
     "assert";
     "Type0";
+    "unit";
   ]
 
 let fstar_int_name (int_ty : integer_type) =
@@ -304,10 +305,14 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   | Adt (type_id, tys) -> (
       match type_id with
       | Tuple ->
-          F.pp_print_string fmt "(";
-          Collections.List.iter_link (F.pp_print_space fmt)
-            (extract_ty ctx fmt true) tys;
-          F.pp_print_string fmt ")"
+          (* This is a bit annoying, but in F* `()` is not the unit type:
+           * we have to write `unit`... *)
+          if tys = [] then F.pp_print_string fmt "unit"
+          else (
+            F.pp_print_string fmt "(";
+            Collections.List.iter_link (F.pp_print_space fmt)
+              (extract_ty ctx fmt true) tys;
+            F.pp_print_string fmt ")")
       | AdtId _ | Assumed _ ->
           if inside then F.pp_print_string fmt "(";
           F.pp_print_string fmt (ctx_get_type type_id ctx);
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index cbc2409d..1ef4b325 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -633,7 +633,9 @@ let to_monadic (def : fun_def) : fun_def =
       let id, _ = VarId.fresh var_cnt in
       let var = { id; basename = None; ty = unit_ty } in
       let inputs = [ var ] in
-      { def with signature; inputs })
+      let input_lv = mk_typed_lvalue_from_var var None in
+      let inputs_lvs = [ input_lv ] in
+      { def with signature; inputs; inputs_lvs })
     else def
   in
   (* Then the output type *)
-- 
cgit v1.2.3