diff options
| -rw-r--r-- | compiler/Extract.ml | 69 |
1 files changed, 15 insertions, 54 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index f3061273..787929fd 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1498,9 +1498,6 @@ let extract_global_decl_register_names (ctx : extraction_ctx) TODO: we don't need something very generic anymore (some definitions used to be polymorphic). - - TODO: this does roughly the same thing as extract_adt_cons -- make the - latter call the former *) let extract_adt_g_value (extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx) @@ -1508,8 +1505,10 @@ let extract_adt_g_value (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) : extraction_ctx = match ty with - | Adt (Tuple, _) -> + | Adt (Tuple, type_args) -> (* Tuple *) + (* For now, we only support fully applied tuple constructors *) + assert (List.length type_args = List.length field_values); (* This is very annoying: in Coq, we can't write [()] for the value of type [unit], we have to write [tt]. *) if !backend = Coq && field_values = [] then ( @@ -1547,7 +1546,8 @@ let extract_adt_g_value | _ -> ctx_get_variant adt_id vid ctx) | None -> ctx_get_struct with_opaque_pre adt_id ctx in - if inside && field_values <> [] then F.pp_print_string fmt "("; + let use_parentheses = inside && field_values <> [] in + if use_parentheses then F.pp_print_string fmt "("; F.pp_print_string fmt cons; let ctx = Collections.List.fold_left @@ -1556,7 +1556,7 @@ let extract_adt_g_value extract_value ctx true v) ctx field_values in - if inside && field_values <> [] then F.pp_print_string fmt ")"; + if use_parentheses then F.pp_print_string fmt ")"; ctx | _ -> raise (Failure "Inconsistent typed value") @@ -1717,54 +1717,15 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (adt_cons : adt_cons_id) (type_args : ty list) (args : texpression list) : unit = - match adt_cons.adt_id with - | Tuple -> - (* Tuple *) - (* For now, we only support fully applied tuple constructors *) - (* This is very annoying: in Coq, we can't write [()] for the value of - type [unit], we have to write [tt]. *) - assert (List.length type_args = List.length args); - if !backend = Coq && args = [] then F.pp_print_string fmt "tt" - else ( - F.pp_print_string fmt "("; - Collections.List.iter_link - (fun () -> - F.pp_print_string fmt ","; - F.pp_print_space fmt ()) - (fun v -> extract_texpression ctx fmt false v) - args; - F.pp_print_string fmt ")") - | _ -> - (* TODO: this duplicates [extrac_adt_g_value] *) - (* "Regular" ADT *) - (* We print something of the form: [Cons field0 ... fieldn]. - * We could update the code to print something of the form: - * [{ field0=...; ...; fieldn=...; }] in case of fully - * applied structure constructors. - *) - let cons = - (* The ADT shouldn't be opaque *) - let with_opaque_pre = false in - match adt_cons.variant_id with - | Some vid -> ( - (* In the case of Lean, we might have to add the type name as a prefix *) - match (!backend, adt_cons.adt_id) with - | Lean, Assumed _ -> - ctx_get_type with_opaque_pre adt_cons.adt_id ctx - ^ "." - ^ ctx_get_variant adt_cons.adt_id vid ctx - | _ -> ctx_get_variant adt_cons.adt_id vid ctx) - | None -> ctx_get_struct with_opaque_pre adt_cons.adt_id ctx - in - let use_parentheses = inside && args <> [] in - if use_parentheses then F.pp_print_string fmt "("; - F.pp_print_string fmt cons; - Collections.List.iter - (fun v -> - F.pp_print_space fmt (); - extract_texpression ctx fmt true v) - args; - if use_parentheses then F.pp_print_string fmt ")" + let e_ty = Adt (adt_cons.adt_id, type_args) in + let _ = + extract_adt_g_value + (fun ctx inside e -> + extract_texpression ctx fmt inside e; + ctx) + fmt ctx inside adt_cons.variant_id args e_ty + in + () (** Subcase of the app case: ADT field projector. *) and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) |