From af78286d801b26bf7a70b8815619591d48245cb8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 Oct 2023 12:23:26 +0200
Subject: Slightly improve formatting of the generated code

---
 compiler/Extract.ml          |  7 ++++++-
 tests/lean/Traits/Types.lean | 20 ++++++++++----------
 2 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 19c3803b..ce423acf 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -4272,6 +4272,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
       let item_name = ctx_get_trait_const decl.def_id name ctx in
       let ty () =
         let inside = false in
+        F.pp_print_space fmt ();
         extract_ty ctx fmt TypeDeclId.Set.empty inside ty
       in
       extract_trait_decl_item ctx fmt item_name ty)
@@ -4282,7 +4283,10 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (fun (name, (clauses, _)) ->
       (* Extract the type *)
       let item_name = ctx_get_trait_type decl.def_id name ctx in
-      let ty () = F.pp_print_string fmt (type_keyword ()) in
+      let ty () =
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt (type_keyword ())
+      in
       extract_trait_decl_item ctx fmt item_name ty;
       (* Extract the clauses *)
       List.iter
@@ -4291,6 +4295,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
             ctx_get_trait_item_clause decl.def_id name clause.clause_id ctx
           in
           let ty () =
+            F.pp_print_space fmt ();
             extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
           in
           extract_trait_decl_item ctx fmt item_name ty)
diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean
index b3a52346..a8c12fe5 100644
--- a/tests/lean/Traits/Types.lean
+++ b/tests/lean/Traits/Types.lean
@@ -48,11 +48,11 @@ structure BoolWrapper where
 
 /- Trait declaration: [traits::WithConstTy] -/
 structure WithConstTy (Self : Type) (LEN : Usize) where
-  LEN1 :Usize
-  LEN2 :Usize
-  V :Type
-  W :Type
-  W_clause_0 :ToU64 W
+  LEN1 : Usize
+  LEN2 : Usize
+  V : Type
+  W : Type
+  W_clause_0 : ToU64 W
   f : W → Array U8 LEN → Result W
 
 /- [alloc::string::String] -/
@@ -60,7 +60,7 @@ axiom alloc.string.String : Type
 
 /- Trait declaration: [traits::ParentTrait0] -/
 structure ParentTrait0 (Self : Type) where
-  W :Type
+  W : Type
   get_name : Self → Result alloc.string.String
   get_w : Self → Result W
 
@@ -74,13 +74,13 @@ structure ChildTrait (Self : Type) where
 
 /- Trait declaration: [traits::Iterator] -/
 structure Iterator (Self : Type) where
-  Item :Type
+  Item : Type
 
 /- Trait declaration: [traits::IntoIterator] -/
 structure IntoIterator (Self : Type) where
-  Item :Type
-  IntoIter :Type
-  IntoIter_clause_0 :Iterator IntoIter
+  Item : Type
+  IntoIter : Type
+  IntoIter_clause_0 : Iterator IntoIter
   into_iter : Self → Result IntoIter
 
 end traits
-- 
cgit v1.2.3