diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 164 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 3 |
2 files changed, 100 insertions, 67 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index aef37a86..01bd5d38 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -681,15 +681,20 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) in let field_name (def_name : name) (field_id : FieldId.id) (field_name : string option) : string = - let field_name = + let field_name_s = match field_name with | Some field_name -> field_name - | None -> FieldId.to_string field_id + | None -> + (* TODO: extract structs with no field names to tuples *) + FieldId.to_string field_id in - if !Config.record_fields_short_names then field_name + if !Config.record_fields_short_names then + if field_name = None then (* TODO: this is a bit ugly *) + "_" ^ field_name_s + else field_name_s else let def_name = type_name_to_snake_case def_name ^ "_" in - def_name ^ field_name + def_name ^ field_name_s in let variant_name (def_name : name) (variant : string) : string = match !backend with @@ -894,7 +899,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) let trait_clause_basename (_varset : StringSet.t) (_clause : trait_clause) : string = (* TODO: actually use the clause to derive the name *) - "cl" + "inst" in let trait_self_clause_basename = "self_clause" in let append_index (basename : string) (i : int) : string = @@ -1330,6 +1335,17 @@ and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter) extract_generic_args ctx fmt no_params_tys tr.generics; if use_brackets then F.pp_print_string fmt ")" +and extract_trait_decl_ref (ctx : extraction_ctx) (fmt : F.formatter) + (no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_decl_ref) : + unit = + let use_brackets = tr.decl_generics <> empty_generic_args && inside in + let is_opaque = false in + let name = ctx_get_trait_decl is_opaque tr.trait_decl_id ctx in + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt name; + extract_generic_args ctx fmt no_params_tys tr.decl_generics; + if use_brackets then F.pp_print_string fmt ")" + and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (generics : generic_args) : unit = let { types; const_generics; trait_refs } = generics in @@ -1734,8 +1750,9 @@ let extract_trait_self_clause (insert_req_space : unit -> unit) method and need to insert a trait self clause (see {!TraitSelfClauseId}). *) let extract_generic_params (ctx : extraction_ctx) (fmt : F.formatter) - (no_params_tys : TypeDeclId.Set.t) (use_forall : bool) (as_implicits : bool) - (space : bool ref option) (trait_decl : trait_decl option) + (no_params_tys : TypeDeclId.Set.t) ?(use_forall = false) + ?(use_forall_use_sep = true) ?(as_implicits : bool = false) + ?(space : bool ref option = None) ?(trait_decl : trait_decl option = None) (generics : generic_params) (type_params : string list) (cg_params : string list) (trait_clauses : string list) : unit = let all_params = List.concat [ type_params; cg_params; trait_clauses ] in @@ -1757,9 +1774,10 @@ let extract_generic_params (ctx : extraction_ctx) (fmt : F.formatter) (* Print the type/const generic parameters *) if all_params <> [] then ( if use_forall then ( + if use_forall_use_sep then ( + insert_req_space (); + F.pp_print_string fmt ":"); insert_req_space (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); F.pp_print_string fmt "forall"); (* Small helper - we may need to split the parameters *) let print_generics (type_params : string list) @@ -1917,9 +1935,8 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) support trait clauses *) assert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4); (* Print the generic parameters *) - let as_implicits = false in - extract_generic_params ctx_body fmt type_decl_group use_forall as_implicits - None None def.generics type_params cg_params trait_clauses; + extract_generic_params ctx_body fmt type_decl_group ~use_forall def.generics + type_params cg_params trait_clauses; (* Print the "=" if we extract the body*) if extract_body then ( F.pp_print_space fmt (); @@ -2149,11 +2166,9 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in F.pp_print_string fmt field_name; (* Print the generics *) - let use_forall = false in let as_implicits = true in - extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall - as_implicits None None decl.generics type_params cg_params - trait_clauses; + extract_generic_params ctx fmt TypeDeclId.Set.empty ~as_implicits + decl.generics type_params cg_params trait_clauses; (* Print the record parameter *) F.pp_print_space fmt (); F.pp_print_string fmt "("; @@ -3220,11 +3235,9 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) (* Print the generics *) (* Open a box for the generics *) F.pp_open_hovbox fmt 0; - let use_forall = false in - let as_implicits = false in - extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall as_implicits - (Some space) trait_decl def.signature.generics type_params cg_params - trait_clauses; + (let space = Some space in + extract_generic_params ctx fmt TypeDeclId.Set.empty ~space ~trait_decl + def.signature.generics type_params cg_params trait_clauses); (* Close the box for the generics *) F.pp_close_box fmt (); (* The input parameters - note that doing this adds bindings to the context *) @@ -4064,14 +4077,13 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) let extract_trait_item (ctx : extraction_ctx) (fmt : F.formatter) (item_name : string) (separator : string) (ty : unit -> unit) : unit = F.pp_print_space fmt (); - F.pp_open_vbox fmt ctx.indent_incr; + F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt item_name; F.pp_print_space fmt (); (* ":" or "=" *) F.pp_print_string fmt separator; - F.pp_print_space fmt (); ty (); - F.pp_print_string fmt ";"; + (match !Config.backend with Lean -> () | _ -> F.pp_print_string fmt ";"); F.pp_close_box fmt () let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter) @@ -4080,7 +4092,8 @@ let extract_trait_decl_item (ctx : extraction_ctx) (fmt : F.formatter) let extract_trait_impl_item (ctx : extraction_ctx) (fmt : F.formatter) (item_name : string) (ty : unit -> unit) : unit = - extract_trait_item ctx fmt item_name "=" ty + let assign = match !Config.backend with Lean -> ":=" | _ -> "=" in + extract_trait_item ctx fmt item_name assign ty (** Small helper - TODO: move *) let generic_params_drop_prefix (g1 : generic_params) (g2 : generic_params) : @@ -4115,9 +4128,9 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter) ctx_add_generic_params generics ctx in let use_forall = generics <> empty_generic_params in - let use_implicits = false in - extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall - use_implicits None None generics type_params cg_params trait_clauses; + let use_forall_use_sep = false in + extract_generic_params ctx fmt TypeDeclId.Set.empty ~use_forall + ~use_forall_use_sep generics type_params cg_params trait_clauses; if use_forall then F.pp_print_string fmt ","; (* Extract the inputs and output *) F.pp_print_space fmt (); @@ -4136,23 +4149,29 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt [ "[" ^ Print.name_to_string decl.name ^ "]" ]; + extract_comment fmt + [ "Trait declaration: [" ^ Print.name_to_string decl.name ^ "]" ]; F.pp_print_break fmt 0 0; - (* Open two boxes for the definition, so that whenever possible it gets printed on - * one line and indents are correct *) - F.pp_open_hvbox fmt 0; - F.pp_open_vbox fmt ctx.indent_incr; + (* Open two outer boxes for the definition, so that whenever possible it gets printed on + one line and indents are correct. + + There is just an exception with Lean: in this backend, line breaks are important + for the parsing, so we always open a vertical box. + *) + if !Config.backend = Lean then F.pp_open_vbox fmt ctx.indent_incr + else ( + F.pp_open_hvbox fmt 0; + F.pp_open_hvbox fmt ctx.indent_incr); (* `struct Trait (....) =` *) (* Open the box for the name + generics *) - F.pp_open_vbox fmt ctx.indent_incr; + F.pp_open_hovbox fmt ctx.indent_incr; let qualif = Option.get (ctx.fmt.type_decl_kind_to_qualif SingleNonRec (Some Struct)) in F.pp_print_string fmt qualif; F.pp_print_space fmt (); F.pp_print_string fmt decl_name; - (* Print the generics *) (* We ignore the trait clauses, which we extract as *fields* *) let generics = { decl.generics with trait_clauses = [] } in @@ -4161,13 +4180,13 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) let ctx, type_params, cg_params, trait_clauses = ctx_add_generic_params generics ctx in - let use_forall = false in - let as_implicits = false in - extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall as_implicits - None None generics type_params cg_params trait_clauses; + extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params + cg_params trait_clauses; F.pp_print_space fmt (); - F.pp_print_string fmt "{"; + (match !backend with + | Lean -> F.pp_print_string fmt "where" + | _ -> F.pp_print_string fmt "{"); (* Close the box for the name + generics *) F.pp_close_box fmt (); @@ -4225,11 +4244,14 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) decl.required_methods; (* Close the brackets *) - F.pp_print_space fmt (); - F.pp_print_string fmt "}"; + (match !Config.backend with + | Lean -> () + | _ -> + F.pp_print_space fmt (); + F.pp_print_string fmt "}"); - (* Close the two outer boxes for the definition *) - F.pp_close_box fmt (); + (* Close the outer boxes for the definition *) + if !Config.backend <> Lean then F.pp_close_box fmt (); F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 @@ -4258,9 +4280,8 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter) in let ctx, f_tys, f_cgs, f_tcs = ctx_add_generic_params f_generics ctx in let use_forall = f_generics <> empty_generic_params in - let use_implicits = false in - extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall - use_implicits None None f_generics f_tys f_cgs f_tcs; + extract_generic_params ctx fmt TypeDeclId.Set.empty ~use_forall f_generics + f_tys f_cgs f_tcs; if use_forall then F.pp_print_string fmt ","; (* Extract the function call *) F.pp_print_space fmt (); @@ -4289,19 +4310,27 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment fmt [ "[" ^ Print.name_to_string impl.name ^ "]" ]; + extract_comment fmt + [ "Trait implementation: [" ^ Print.name_to_string impl.name ^ "]" ]; F.pp_print_break fmt 0 0; - (* Open two boxes for the definition, so that whenever possible it gets printed on - * one line and indents are correct *) - F.pp_open_hvbox fmt 0; - F.pp_open_vbox fmt ctx.indent_incr; - (* `let Trait (....) =` *) + (* Open two outer boxes for the definition, so that whenever possible it gets printed on + one line and indents are correct. + + There is just an exception with Lean: in this backend, line breaks are important + for the parsing, so we always open a vertical box. + *) + if !Config.backend = Lean then ( + F.pp_open_vbox fmt 0; + F.pp_open_vbox fmt ctx.indent_incr) + else ( + F.pp_open_hvbox fmt 0; + F.pp_open_hvbox fmt ctx.indent_incr); + + (* `let (....) : Trait ... =` *) (* Open the box for the name + generics *) - F.pp_open_vbox fmt ctx.indent_incr; - let qualif = - Option.get (ctx.fmt.type_decl_kind_to_qualif SingleNonRec None) - in + F.pp_open_hovbox fmt ctx.indent_incr; + let qualif = Option.get (ctx.fmt.fun_decl_kind_to_qualif SingleNonRec) in F.pp_print_string fmt qualif; F.pp_print_space fmt (); F.pp_print_string fmt impl_name; @@ -4313,13 +4342,18 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) ctx_add_generic_params impl.generics ctx in let all_generics = (type_params, cg_params, trait_clauses) in - let use_forall = false in - let as_implicits = false in - extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall as_implicits - None None impl.generics type_params cg_params trait_clauses; + extract_generic_params ctx fmt TypeDeclId.Set.empty impl.generics type_params + cg_params trait_clauses; + + (* Print the type *) + F.pp_print_space fmt (); + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + extract_trait_decl_ref ctx fmt TypeDeclId.Set.empty false impl.impl_trait; F.pp_print_space fmt (); - F.pp_print_string fmt "{"; + if !Config.backend = Lean then F.pp_print_string fmt ":= {" + else F.pp_print_string fmt "= {"; (* Close the box for the name + generics *) F.pp_close_box fmt (); @@ -4374,12 +4408,10 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) extract_trait_impl_method_items ctx fmt impl name id all_generics) impl.required_methods; - (* Close the brackets *) + (* Close the outer boxes for the definition, as well as the brackets *) + F.pp_close_box fmt (); F.pp_print_space fmt (); F.pp_print_string fmt "}"; - - (* Close the two outer boxes for the definition *) - F.pp_close_box fmt (); F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 4238d9af..a81ec052 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -952,7 +952,8 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string = in log#serror err; if !Config.extract_fail_hard then raise (Failure err) - else "(ERROR: \"" ^ id_to_string id ctx ^ "\")") + else + "(%%%ERROR: unknown identifier\": " ^ id_to_string id ctx ^ "\"%%%)") else let m = ctx.names_map.id_to_name in match IdMap.find_opt id m with |