From 1aa2d3e0584d9f360e085f6d81ecf5a3e741ad94 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Feb 2022 21:24:04 +0100
Subject: Fix more issues

---
 src/ExtractToFStar.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 7da5adb8..60bc472d 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -235,7 +235,9 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
                 let def =
                   TypeDefId.Map.find adt_id ctx.type_context.type_defs
                 in
-                StringUtils.string_of_chars [ (get_type_name def.name).[0] ])
+                let c = (get_type_name def.name).[0] in
+                let c = StringUtils.lowercase_ascii c in
+                String.make 1 c)
         | TypeVar _ -> "x" (* lacking imagination here... *)
         | Bool -> "b"
         | Char -> "c"
@@ -715,7 +717,11 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
               extract_ty ctx fmt true ty)
             call.type_params;
           (* Print the input values *)
-          List.iter (fun ve -> extract_texpression ctx fmt true ve) call.args;
+          List.iter
+            (fun ve ->
+              F.pp_print_space fmt ();
+              extract_texpression ctx fmt true ve)
+            call.args;
           (* Close the box for the function call *)
           F.pp_close_box fmt ();
           (* Return *)
-- 
cgit v1.2.3