diff options
| -rw-r--r-- | compiler/Extract.ml | 55 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 11 |
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 |