summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Translate.ml295
1 files changed, 194 insertions, 101 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 75fc7fe9..c5f7df92 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -750,18 +750,17 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
if config.extract_state_type && config.extract_fun_decls then
export_state_type ();
- (* For Lean, we parameterize the entire development by a section variable
- called opaque_defs, of type OpaqueDefs. The code below emits the type
- 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.
-
- We also generate such a structure only if there actually are opaque
- definitions.
- *)
+ (* Obsolete: (TODO: remove) For Lean we parameterize the entire development by a section
+ variable called opaque_defs, of type OpaqueDefs. The code below emits the type
+ 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.
+
+ 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
+ config.extract_opaque && config.extract_fun_decls
+ && !Config.wrap_opaque_in_sig
&&
let _, opaque_funs = module_has_opaque_decls ctx in
opaque_funs
@@ -783,11 +782,22 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
if wrap_in_sig then Format.pp_close_box fmt ()
-let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
- (rust_module_name : string) (module_name : string) (custom_msg : string)
- (custom_imports : string list) (custom_includes : string list) : unit =
+type extract_file_info = {
+ filename : string;
+ namespace : string;
+ in_namespace : bool;
+ crate_name : string;
+ rust_module_name : string;
+ module_name : string;
+ custom_msg : string;
+ custom_imports : string list;
+ custom_includes : string list;
+}
+
+let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
+ : unit =
(* Open the file and create the formatter *)
- let out = open_out filename in
+ let out = open_out fi.filename in
let fmt = Format.formatter_of_out_channel out in
(* Print the headers.
@@ -801,19 +811,22 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
(match !Config.backend with
| Lean ->
Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
- Printf.fprintf out "-- [%s]%s\n" rust_module_name custom_msg
+ Printf.fprintf out "-- [%s]%s\n" fi.rust_module_name fi.custom_msg
| Coq | FStar | HOL4 ->
Printf.fprintf out
"(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
- Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg);
+ Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg);
+ (* Generate the imports *)
(match !Config.backend with
| FStar ->
- Printf.fprintf out "module %s\n" module_name;
+ Printf.fprintf out "module %s\n" fi.module_name;
Printf.fprintf out "open Primitives\n";
(* Add the custom imports *)
- List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
+ List.iter (fun m -> Printf.fprintf out "open %s\n" m) fi.custom_imports;
(* Add the custom includes *)
- List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
+ List.iter
+ (fun m -> Printf.fprintf out "include %s\n" m)
+ fi.custom_includes;
(* Z3 options - note that we use fuel 1 because it its useful for the decrease clauses *)
Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 1 --ifuel 1\"\n"
| Coq ->
@@ -825,24 +838,29 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
(* Add the custom imports *)
List.iter
(fun m -> Printf.fprintf out "Require Import %s.\n" m)
- custom_imports;
+ fi.custom_imports;
(* Add the custom includes *)
List.iter
(fun m ->
Printf.fprintf out "Require Export %s.\n" m;
Printf.fprintf out "Import %s.\n" m)
- custom_includes;
- Printf.fprintf out "Module %s.\n" module_name
+ fi.custom_includes;
+ Printf.fprintf out "Module %s.\n" fi.module_name
| Lean ->
- Printf.fprintf out "import Base.Primitives\n";
+ Printf.fprintf out "import Base\n";
(* Add the custom imports *)
- List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
+ List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_imports;
(* Add the custom includes *)
- List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes
+ List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes;
+ (* Always open the Primitives namespace *)
+ Printf.fprintf out "open Primitives\n";
+ (* If we are inside the namespace: declare it, otherwise: open it *)
+ if fi.in_namespace then Printf.fprintf out "namespace %s\n" fi.namespace
+ else Printf.fprintf out "open %s\n" fi.namespace
| HOL4 ->
Printf.fprintf out "open primitivesLib divDefLib\n";
(* Add the custom imports and includes *)
- let imports = custom_imports @ custom_includes in
+ let imports = fi.custom_imports @ fi.custom_includes in
(* The imports are a list of module names: we need to add a "Theory" suffix *)
let imports = List.map (fun s -> s ^ "Theory") imports in
if imports <> [] then
@@ -850,7 +868,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
Printf.fprintf out "open %s\n\n" imports
else Printf.fprintf out "\n";
(* Initialize the theory *)
- Printf.fprintf out "val _ = new_theory \"%s\"\n\n" module_name);
+ Printf.fprintf out "val _ = new_theory \"%s\"\n\n" fi.module_name);
(* From now onwards, we use the formatter *)
(* Set the margin *)
Format.pp_set_margin fmt 80;
@@ -867,12 +885,13 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
(* Close the module *)
(match !Config.backend with
- | FStar | Lean -> ()
+ | FStar -> ()
+ | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
| HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
- | Coq -> Printf.fprintf out "End %s .\n" module_name);
+ | Coq -> Printf.fprintf out "End %s .\n" fi.module_name);
(* Some logging *)
- log#linfo (lazy ("Generated: " ^ filename));
+ log#linfo (lazy ("Generated: " ^ fi.filename));
(* Flush and close the file *)
close_out out
@@ -891,18 +910,24 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
prefixed with the type name to prevent collisions *)
match !Config.backend with Coq | FStar | HOL4 -> true | Lean -> false
in
+ (* Initialize the names map (we insert the names of the "primitives"
+ declarations, and insert the names of the local declarations later) *)
let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in
let fmt, names_map =
mk_formatter_and_names_map trans_ctx crate.name
variant_concatenate_type_name
in
+ (* Put everything in the context *)
let ctx =
{
ExtractBase.trans_ctx;
names_map;
+ unsafe_names_map = { id_to_name = ExtractBase.IdMap.empty };
fmt;
indent_incr = 2;
use_opaque_pre = !Config.split_files;
+ use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
+ fun_name_info = PureUtils.RegularFunIdMap.empty;
}
in
@@ -968,7 +993,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(* Open the output file *)
(* First compute the filename by replacing the extension and converting the
* case (rust module names are snake case) *)
- let module_name, extract_filebasename =
+ let namespace, crate_name, extract_filebasename =
match Filename.chop_suffix_opt ~suffix:".llbc" filename with
| None ->
(* Note that we already checked the suffix upon opening the file *)
@@ -977,14 +1002,20 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(* Retrieve the file basename *)
let basename = Filename.basename filename in
(* Convert the case *)
- let module_name = StringUtils.to_camel_case basename in
- let module_name =
+ let crate_name = StringUtils.to_camel_case basename in
+ let crate_name =
if !Config.backend = HOL4 then
- StringUtils.lowercase_first_letter module_name
- else module_name
+ StringUtils.lowercase_first_letter crate_name
+ else crate_name
+ in
+ (* We use the raw crate name for the namespaces *)
+ let namespace =
+ match !Config.backend with
+ | FStar | Coq | HOL4 -> crate.name
+ | Lean -> crate.name
in
(* Concatenate *)
- (module_name, Filename.concat dest_dir module_name)
+ (namespace, crate_name, Filename.concat dest_dir crate_name)
in
(* Put the translated definitions in maps *)
@@ -1019,11 +1050,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
create more directories *)
if !Config.backend = Lean then (
let ( ^^ ) = Filename.concat in
- mkdir_if (dest_dir ^^ "Base");
- if !Config.split_files then mkdir_if (dest_dir ^^ module_name);
+ if !Config.split_files then mkdir_if (dest_dir ^^ crate_name);
if needs_clauses_module then (
assert !Config.split_files;
- mkdir_if (dest_dir ^^ module_name ^^ "Clauses")));
+ mkdir_if (dest_dir ^^ crate_name ^^ "Clauses")));
(* Copy the "Primitives" file, if necessary *)
let _ =
@@ -1033,7 +1063,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
match !Config.backend with
| FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
| Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
- | Lean -> Some ("/backends/lean/Primitives.lean", "Base/Primitives.lean")
+ | Lean -> None
| HOL4 -> None
in
match primitives_src_dest with
@@ -1117,6 +1147,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(* Extract the types *)
(* If there are opaque types, we extract in an interface *)
+ (* TODO: for Lean and Coq: generate a template file *)
let types_filename_ext =
match !Config.backend with
| FStar -> if has_opaque_types then ".fsti" else ".fst"
@@ -1127,7 +1158,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
let types_filename =
extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
in
- let types_module = module_name ^ module_delimiter ^ "Types" in
+ let types_module = crate_name ^ module_delimiter ^ "Types" in
let types_config =
{
base_gen_config with
@@ -1137,8 +1168,20 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
interface = has_opaque_types;
}
in
- extract_file types_config gen_ctx types_filename crate.A.name types_module
- ": type definitions" [] [];
+ let file_info =
+ {
+ filename = types_filename;
+ namespace;
+ in_namespace = true;
+ crate_name;
+ rust_module_name = crate.A.name;
+ module_name = types_module;
+ custom_msg = ": type definitions";
+ custom_imports = [];
+ custom_includes = [];
+ }
+ in
+ extract_file types_config gen_ctx file_info;
(* Extract the template clauses *)
(if needs_clauses_module && !Config.extract_template_decreases_clauses then
@@ -1147,33 +1190,49 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
^ "Template" ^ ext
in
let template_clauses_module =
- module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter
+ crate_name ^ module_delimiter ^ "Clauses" ^ module_delimiter
^ "Template"
in
let template_clauses_config =
{ base_gen_config with extract_template_decreases_clauses = true }
in
- extract_file template_clauses_config gen_ctx template_clauses_filename
- crate.A.name template_clauses_module
- ": templates for the decreases clauses" [ types_module ] []);
+ let file_info =
+ {
+ filename = template_clauses_filename;
+ namespace;
+ in_namespace = true;
+ crate_name;
+ rust_module_name = crate.A.name;
+ module_name = template_clauses_module;
+ custom_msg = ": templates for the decreases clauses";
+ custom_imports = [ types_module ];
+ custom_includes = [];
+ }
+ in
+ extract_file template_clauses_config gen_ctx file_info);
(* Extract the opaque functions, if needed *)
let opaque_funs_module =
if has_opaque_funs then (
+ (* In the case of Lean we generate a template file *)
+ let module_suffix, opaque_imported_suffix, custom_msg =
+ match !Config.backend with
+ | FStar | Coq | HOL4 ->
+ ("Opaque", "Opaque", ": external function declarations")
+ | Lean ->
+ ( "FunsExternal_Template",
+ "FunsExternal",
+ ": external functions.\n\
+ -- This is a template file: rename it to \
+ \"FunsExternal.lean\" and fill the holes." )
+ in
let opaque_filename =
- extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext
+ extract_filebasename ^ file_delimiter ^ module_suffix ^ opaque_ext
in
- let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
+ let opaque_module = crate_name ^ module_delimiter ^ module_suffix in
let opaque_imported_module =
- (* In the case of Lean, we declare an interface (a record) containing
- the opaque definitions, and we leave it to the user to provide an
- instance of this module.
-
- TODO: do the same for Coq.
- TODO: do the same for the type definitions.
- *)
if !Config.backend = Lean then
- module_name ^ module_delimiter ^ "ExternalFuns"
+ crate_name ^ module_delimiter ^ opaque_imported_suffix
else opaque_module
in
let opaque_config =
@@ -1191,15 +1250,28 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false };
}
in
- extract_file opaque_config gen_ctx opaque_filename crate.A.name
- opaque_module ": opaque function definitions" [] [ types_module ];
+ let file_info =
+ {
+ filename = opaque_filename;
+ namespace;
+ in_namespace = false;
+ crate_name;
+ rust_module_name = crate.A.name;
+ module_name = opaque_module;
+ custom_msg;
+ custom_imports = [];
+ custom_includes = [ types_module ];
+ }
+ in
+ extract_file opaque_config gen_ctx file_info;
+ (* Return the additional dependencies *)
[ opaque_imported_module ])
else []
in
(* Extract the functions *)
let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in
- let fun_module = module_name ^ module_delimiter ^ "Funs" in
+ let fun_module = crate_name ^ module_delimiter ^ "Funs" in
let fun_config =
{
base_gen_config with
@@ -1213,12 +1285,24 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
let clauses_submodule =
if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
in
- [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
+ [ crate_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
else []
in
- extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
- ": function definitions" []
- ([ types_module ] @ opaque_funs_module @ clauses_module))
+ let file_info =
+ {
+ filename = fun_filename;
+ namespace;
+ in_namespace = true;
+ crate_name;
+ rust_module_name = crate.A.name;
+ module_name = fun_module;
+ custom_msg = ": function definitions";
+ custom_imports = [];
+ custom_includes =
+ [ types_module ] @ opaque_funs_module @ clauses_module;
+ }
+ in
+ extract_file fun_config gen_ctx file_info)
else
let gen_config =
{
@@ -1235,10 +1319,21 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
test_trans_unit_functions = !Config.test_trans_unit_functions;
}
in
+ let file_info =
+ {
+ filename = extract_filebasename ^ ext;
+ namespace;
+ in_namespace = true;
+ crate_name;
+ rust_module_name = crate.A.name;
+ module_name = crate_name;
+ custom_msg = "";
+ custom_imports = [];
+ custom_includes = [];
+ }
+ in
(* Add the extension for F* *)
- let extract_filename = extract_filebasename ^ ext in
- extract_file gen_config gen_ctx extract_filename crate.A.name module_name
- "" [] []);
+ extract_file gen_config gen_ctx file_info);
(* Generate the build file *)
match !Config.backend with
@@ -1256,47 +1351,45 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
* different files.
*)
if !Config.split_files then (
- let filename = Filename.concat dest_dir (module_name ^ ".lean") in
+ let filename = Filename.concat dest_dir (crate_name ^ ".lean") in
let out = open_out filename in
(* Write *)
- Printf.fprintf out "import %s.Funs\n" module_name;
+ Printf.fprintf out "import %s.Funs\n" crate_name;
(* Flush and close the file, log *)
close_out out;
log#linfo (lazy ("Generated: " ^ filename)));
(*
- * Generate the lakefile.lean file
+ * Generate the lakefile.lean file, if the user asks for it
*)
+ if !Config.lean_gen_lakefile then (
+ (* Open the file *)
+ let filename = Filename.concat dest_dir "lakefile.lean" in
+ let out = open_out filename in
- (* Open the file *)
- let filename = Filename.concat dest_dir "lakefile.lean" in
- let out = open_out filename in
-
- (* Generate the content *)
- Printf.fprintf out "import Lake\nopen Lake DSL\n\n";
- Printf.fprintf out "require mathlib from git\n";
- Printf.fprintf out
- " \"https://github.com/leanprover-community/mathlib4.git\"\n\n";
-
- let package_name = StringUtils.to_snake_case module_name in
- Printf.fprintf out "package «%s» {}\n\n" package_name;
-
- Printf.fprintf out "lean_lib «Base» {}\n\n";
-
- Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" module_name;
-
- (* No default target for now.
- Format would be:
- {[
- @[default_target]
- lean_exe «package_name» {
- root := `Main
- }
- ]}
- *)
+ (* Generate the content *)
+ Printf.fprintf out "import Lake\nopen Lake DSL\n\n";
+ Printf.fprintf out "require mathlib from git\n";
+ Printf.fprintf out
+ " \"https://github.com/leanprover-community/mathlib4.git\"\n\n";
+
+ let package_name = StringUtils.to_snake_case crate_name in
+ Printf.fprintf out "package «%s» {}\n\n" package_name;
+
+ Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" crate_name;
+
+ (* No default target for now.
+ Format would be:
+ {[
+ @[default_target]
+ lean_exe «package_name» {
+ root := `Main
+ }
+ ]}
+ *)
- (* Flush and close the file *)
- close_out out;
+ (* Flush and close the file *)
+ close_out out;
- (* Logging *)
- log#linfo (lazy ("Generated: " ^ filename))
+ (* Logging *)
+ log#linfo (lazy ("Generated: " ^ filename)))
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 19:29:21 +0000