diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Extract.ml | 14 | ||||
| -rw-r--r-- | compiler/Translate.ml | 166 |
2 files changed, 125 insertions, 55 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index b18d4743..7d00dd73 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1010,6 +1010,11 @@ let end_type_decl_group (fmt : F.formatter) (is_rec : bool) let unit_name () = match !backend with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit" +(** Small helper *) +let extract_arrow (fmt : F.formatter) () : unit = + if !Config.backend = Lean then F.pp_print_string fmt "→" + else F.pp_print_string fmt "->" + (** [inside] constrols whether we should add parentheses or not around type applications (if [true] we add parentheses). @@ -1103,7 +1108,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) if inside then F.pp_print_string fmt "("; extract_rec false arg_ty; F.pp_print_space fmt (); - F.pp_print_string fmt "->"; + extract_arrow fmt (); F.pp_print_space fmt (); extract_rec false ret_ty; if inside then F.pp_print_string fmt ")" @@ -1191,7 +1196,7 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter) (* Print the arrow [->] *) if !backend <> HOL4 then ( F.pp_print_space fmt (); - F.pp_print_string fmt "->"); + extract_arrow fmt ()); (* Close the field box *) F.pp_close_box fmt (); (* Return *) @@ -2268,7 +2273,8 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) ctx xl in F.pp_print_space fmt (); - F.pp_print_string fmt "->"; + if !backend = Lean then F.pp_print_string fmt "=>" + else F.pp_print_string fmt "->"; F.pp_print_space fmt (); (* Print the body *) extract_texpression ctx fmt false e; @@ -2750,7 +2756,7 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx) let inside = false in extract_ty ctx fmt TypeDeclId.Set.empty inside ty; F.pp_print_space fmt (); - F.pp_print_string fmt "->"; + extract_arrow fmt (); F.pp_print_space fmt () in List.iter extract_param def.signature.inputs diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 39b169c9..5827b4a8 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -783,11 +783,20 @@ 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; + 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 +810,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,26 +837,28 @@ 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\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" + Printf.fprintf out "open Primitives\n\n"; + (* Open the namespace *) + Printf.fprintf out "namespace %s\n" fi.crate_name | 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 @@ -852,7 +866,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; @@ -869,12 +883,13 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (* Close the module *) (match !Config.backend with - | FStar | Lean -> () + | FStar -> () + | Lean -> Printf.fprintf out "end %s\n" fi.crate_name | 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 @@ -971,7 +986,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 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 *) @@ -980,14 +995,14 @@ 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 (* Concatenate *) - (module_name, Filename.concat dest_dir module_name) + (crate_name, Filename.concat dest_dir crate_name) in (* Put the translated definitions in maps *) @@ -1022,10 +1037,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : create more directories *) if !Config.backend = Lean then ( let ( ^^ ) = Filename.concat in - 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 _ = @@ -1129,7 +1144,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 @@ -1139,8 +1154,18 @@ 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; + 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 @@ -1149,15 +1174,24 @@ 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; + 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 = @@ -1165,7 +1199,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : let opaque_filename = extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext in - let opaque_module = module_name ^ module_delimiter ^ "Opaque" in + let opaque_module = crate_name ^ module_delimiter ^ "Opaque" 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 @@ -1175,7 +1209,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : TODO: do the same for the type definitions. *) if !Config.backend = Lean then - module_name ^ module_delimiter ^ "ExternalFuns" + crate_name ^ module_delimiter ^ "ExternalFuns" else opaque_module in let opaque_config = @@ -1193,15 +1227,26 @@ 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; + crate_name; + rust_module_name = crate.A.name; + module_name = opaque_module; + custom_msg = ": opaque function definitions"; + 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 @@ -1215,12 +1260,22 @@ 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; + 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 = { @@ -1237,10 +1292,19 @@ 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; + 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 @@ -1258,10 +1322,10 @@ 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))); @@ -1280,10 +1344,10 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : Printf.fprintf out " \"https://github.com/leanprover-community/mathlib4.git\"\n\n"; - let package_name = StringUtils.to_snake_case module_name in + 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" module_name; + Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" crate_name; (* No default target for now. Format would be: |