diff options
| -rw-r--r-- | compiler/Extract.ml | 10 | ||||
| -rw-r--r-- | compiler/Translate.ml | 16 |
2 files changed, 23 insertions, 3 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 8ad87c8e..e5710394 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -183,6 +183,7 @@ let keywords () = "unsafe"; "where"; "with"; + "opaque_defs"; ] in List.concat [ named_unops; named_binops; misc ] @@ -738,11 +739,18 @@ let mk_formatter_and_names_map (ctx : trans_ctx) (crate_name : string) let names_map = initialize_names_map fmt (names_map_init ()) in (fmt, names_map) -(** In Coq, a group of definitions must be ended with a "." *) +(** In some provers, groups of definitions must be delimited. + + - in Coq, *every* group (including singletons) must end with "." + - in Lean, groups of mutually recursive definitions must end with "end" + *) let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) = if !backend = Coq && decl_is_last_from_group kind then ( F.pp_print_cut fmt (); F.pp_print_string fmt ".") + else if !backend = Lean && kind = MutRecLast then ( + F.pp_print_cut fmt (); + F.pp_print_string fmt "end") let unit_name () = match !backend with Lean -> "Unit" | Coq | FStar -> "unit" diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 781766ee..8250f813 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -686,14 +686,26 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) definition for OpaqueDefs, which is a structure, in which each field is one of the functions marked as Opaque. We emit the `structure ...` bit here, then rely on `extract_fun_decl` to be aware of this, and skip the keyword - (e.g. "axiom" or "val") so as to generate valid syntax for records. *) + (e.g. "axiom" or "val") so as to generate valid syntax for records. + + We also generate such a structure only if there actually are opaque + definitions. + *) let wrap_in_sig = config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean + && + let _, opaque_funs = module_has_opaque_decls ctx in + opaque_funs in if wrap_in_sig then ( + (* We change the name of the structure depending on whether we *only* + extract opaque definitions, or if we extract all definitions *) + let struct_name = + if config.extract_transparent then "Definitions" else "OpaqueDefs" + in Format.pp_print_break fmt 0 0; Format.pp_open_vbox fmt ctx.extract_ctx.indent_incr; - Format.pp_print_string fmt "structure OpaqueDefs where"; + Format.pp_print_string fmt ("structure " ^ struct_name ^ " where"); Format.pp_print_break fmt 0 0); List.iter export_decl_group ctx.crate.declarations; |