summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/Extract.ml10
-rw-r--r--compiler/Translate.ml16
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;