summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-12-07 12:23:57 +0100
committerSon Ho2023-12-07 12:23:57 +0100
commit6dbe9e153043e5091a4d17da9bc7c3ed7d4093b1 (patch)
treeb007b79e82a7f0f46f047237c04f210d00e6ddef /compiler
parent0209fee47a11b371d258fe02b8cc59b325de21d6 (diff)
Fix minor issues when extracting a structure with one field as a tuple
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml55
-rw-r--r--compiler/ExtractTypes.ml11
2 files changed, 45 insertions, 21 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 85bdd929..20cdb20b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -531,28 +531,41 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
* projection ([x.field] instead of [MkAdt?.field x] *)
match args with
| [ arg ] ->
- (* Exactly one argument: pretty-print *)
- let field_name =
- (* Check if we need to extract the type as a structure *)
- if
- PureUtils.type_decl_from_type_id_is_tuple_struct
- ctx.trans_ctx.type_ctx.type_infos proj.adt_id
- then FieldId.to_string proj.field_id
- else ctx_get_field proj.adt_id proj.field_id ctx
+ let is_tuple_struct =
+ PureUtils.type_decl_from_type_id_is_tuple_struct
+ ctx.trans_ctx.type_ctx.type_infos proj.adt_id
in
- (* Open a box *)
- F.pp_open_hovbox fmt ctx.indent_incr;
- (* Extract the expression *)
- extract_texpression ctx fmt true arg;
- (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
- if !backend <> Lean then F.pp_print_break fmt 0 0;
- F.pp_print_string fmt ".";
- (* If in Coq, the field projection has to be parenthesized *)
- (match !backend with
- | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
- | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
- (* Close the box *)
- F.pp_close_box fmt ()
+ (* Check if we extract the type as a tuple, and it only has one field.
+ In this case, there is no projection. *)
+ let has_one_field =
+ match proj.adt_id with
+ | TAdtId id -> (
+ let d = TypeDeclId.Map.find id ctx.trans_types in
+ match d.kind with Struct [ _ ] -> true | _ -> false)
+ | _ -> false
+ in
+ if is_tuple_struct && has_one_field then
+ extract_texpression ctx fmt inside arg
+ else
+ (* Exactly one argument: pretty-print *)
+ let field_name =
+ (* Check if we need to extract the type as a tuple *)
+ if is_tuple_struct then FieldId.to_string proj.field_id
+ else ctx_get_field proj.adt_id proj.field_id ctx
+ in
+ (* Open a box *)
+ F.pp_open_hovbox fmt ctx.indent_incr;
+ (* Extract the expression *)
+ extract_texpression ctx fmt true arg;
+ (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
+ if !backend <> Lean then F.pp_print_break fmt 0 0;
+ F.pp_print_string fmt ".";
+ (* If in Coq, the field projection has to be parenthesized *)
+ (match !backend with
+ | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
+ | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
+ (* Close the box *)
+ F.pp_close_box fmt ()
| arg :: args ->
(* Call extract_App again, but in such a way that the first argument is
* isolated *)
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 22243a4a..08064a06 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1287,6 +1287,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
+ in
let type_kind =
if extract_body then
if is_tuple_struct then Some Tuple
@@ -1329,6 +1332,14 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
if is_tuple_struct then F.pp_open_hvbox fmt 0 else F.pp_open_vbox fmt 0);
(* Open a box for "type TYPE_NAME (TYPE_PARAMS CONST_GEN_PARAMS) =" *)
F.pp_open_hovbox fmt ctx.indent_incr;
+ (* > "@[reducible]"
+ 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 (
+ F.pp_print_string fmt "@[reducible]";
+ F.pp_print_space fmt ())
+ else ();
(* > "type TYPE_NAME" *)
let qualif = type_decl_kind_to_qualif kind type_kind in
(match qualif with