diff options
author | Son HO | 2023-07-31 16:15:58 +0200 |
---|---|---|
committer | GitHub | 2023-07-31 16:15:58 +0200 |
commit | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (patch) | |
tree | 92d6021eb549f7cc25501856edd58859786b7e90 /compiler/Translate.ml | |
parent | 53adf30fe440eb8b6f58ba89f4a4c0acc7877498 (diff) | |
parent | 9b3a58e423333fc9a4a5a264c3beb0a3d951e86b (diff) |
Merge pull request #31 from AeneasVerif/son_lean_backend
Improve the Lean backend
Diffstat (limited to 'compiler/Translate.ml')
-rw-r--r-- | compiler/Translate.ml | 295 |
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))) |