summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/ExtractTypes.ml30
1 files changed, 18 insertions, 12 deletions
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 08064a06..785f7629 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -915,15 +915,20 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
(** Extract a struct as a tuple *)
let extract_type_decl_tuple_struct_body (ctx : extraction_ctx)
(fmt : F.formatter) (fields : field list) : unit =
- let sep = match !backend with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
- Collections.List.iter_link
- (fun () ->
- F.pp_print_space fmt ();
- F.pp_print_string fmt sep)
- (fun (f : field) ->
- F.pp_print_space fmt ();
- extract_ty ctx fmt TypeDeclId.Set.empty true f.field_ty)
- fields
+ (* If the type is empty, we need to have a special treatment *)
+ if fields = [] then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt (unit_name ()))
+ else
+ let sep = match !backend with Coq | FStar | HOL4 -> "*" | Lean -> "×" in
+ Collections.List.iter_link
+ (fun () ->
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt sep)
+ (fun (f : field) ->
+ F.pp_print_space fmt ();
+ extract_ty ctx fmt TypeDeclId.Set.empty true f.field_ty)
+ fields
let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
@@ -1287,8 +1292,9 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
TypesUtils.type_decl_from_decl_id_is_tuple_struct
ctx.trans_ctx.type_ctx.type_infos def.def_id
in
- let is_tuple_struct_one_field =
- is_tuple_struct && match def.kind with Struct [ _ ] -> true | _ -> false
+ let is_tuple_struct_one_or_zero_field =
+ is_tuple_struct
+ && match def.kind with Struct [] | Struct [ _ ] -> true | _ -> false
in
let type_kind =
if extract_body then
@@ -1336,7 +1342,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
We need this annotation, otherwise Lean sometimes doesn't manage to typecheck
the expressions when it needs to coerce the type.
*)
- if is_tuple_struct_one_field && !backend = Lean then (
+ if is_tuple_struct_one_or_zero_field && !backend = Lean then (
F.pp_print_string fmt "@[reducible]";
F.pp_print_space fmt ())
else ();