diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 103 |
1 files changed, 60 insertions, 43 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index df7a750d..1c0bcf73 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -466,10 +466,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let is_opaque = Option.is_none body.Pure.body in if - config.extract_globals && ( - ((not is_opaque) && config.extract_transparent) - || (is_opaque && config.extract_opaque) - ) + config.extract_globals + && (((not is_opaque) && config.extract_transparent) + || (is_opaque && config.extract_opaque)) then Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface @@ -564,7 +563,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let has_decr_clause = has_decreases_clause decl in if has_decr_clause then if !Config.backend = Lean then - Extract.extract_termination_and_decreasing ctx.extract_ctx fmt decl + Extract.extract_termination_and_decreasing ctx.extract_ctx fmt + decl else Extract.extract_template_decreases_clause ctx.extract_ctx fmt decl in @@ -661,24 +661,22 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) *) if config.extract_state_type && config.extract_fun_decls then export_state_type (); - if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean then begin + if config.extract_opaque && config.extract_fun_decls && !Config.backend = Lean + then ( 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_break fmt 0 0 - end; + Format.pp_print_break fmt 0 0); List.iter export_decl_group ctx.crate.declarations; - if config.extract_opaque && !Config.backend = Lean then begin - Format.pp_close_box fmt () - end; + if config.extract_opaque && !Config.backend = Lean then + Format.pp_close_box fmt (); if config.extract_state_type && not config.extract_fun_decls then export_state_type () let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (rust_module_name : string) (module_name : string) (custom_msg : string) - ?(custom_variables: string list = []) - (custom_imports : string list) (custom_includes : string list) - : unit = + ?(custom_variables : string list = []) (custom_imports : string list) + (custom_includes : string list) : unit = (* Open the file and create the formatter *) let out = open_out filename in let fmt = Format.formatter_of_out_channel out in @@ -691,14 +689,14 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) * internal count is consistent with the state of the file. *) (* Create the header *) - begin match !Config.backend with + (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" rust_module_name custom_msg | Coq | FStar -> - Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; - Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg - end; + Printf.fprintf out + "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; + Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg); (match !Config.backend with | FStar -> Printf.fprintf out "module %s\n" module_name; @@ -732,11 +730,9 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports; (* Add the custom includes *) List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes; - if custom_variables <> [] then begin + if custom_variables <> [] then ( Printf.fprintf out "\n"; - List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables - end - ); + List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables)); (* From now onwards, we use the formatter *) (* Set the margin *) Format.pp_set_margin fmt 80; @@ -885,13 +881,11 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : (* Lean reflects the module hierarchy within the filesystem, so we need to create more directories *) - if !Config.backend = Lean then begin - let (^^) = Filename.concat in + if !Config.backend = Lean then ( + let ( ^^ ) = Filename.concat in mkdir_if (dest_dir ^^ "Base"); mkdir_if (dest_dir ^^ module_name); - if needs_clauses_module then - mkdir_if (dest_dir ^^ module_name ^^ "Clauses"); - end; + if needs_clauses_module then mkdir_if (dest_dir ^^ module_name ^^ "Clauses")); (* Copy the "Primitives" file *) let _ = @@ -936,7 +930,17 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : let file_delimiter = if !Config.backend = Lean then "/" else module_delimiter in - let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" in + (* File extension for the "regular" modules *) + let ext = + match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" + in + (* File extension for the opaque module *) + let opaque_ext = + match !Config.backend with + | FStar -> ".fsti" + | Coq -> ".v" + | Lean -> ".lean" + in (* Extract one or several files, depending on the configuration *) if !Config.split_files then ( @@ -985,20 +989,28 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : ": type definitions" [] []; (* Extract the template clauses *) - if needs_clauses_module && !Config.extract_template_decreases_clauses then ( - let clauses_filename = extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter ^ "Template" ^ ext in - let clauses_module = module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" in - let clauses_config = - { base_gen_config with extract_template_decreases_clauses = true } - in - extract_file clauses_config gen_ctx clauses_filename crate.A.name - clauses_module ": templates for the decreases clauses" [ types_module ] - []); + (if needs_clauses_module && !Config.extract_template_decreases_clauses then + let template_clauses_filename = + extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter + ^ "Template" ^ ext + in + let template_clauses_module = + module_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 ] []); (* Extract the opaque functions, if needed *) let opaque_funs_module = if has_opaque_funs then ( - let opaque_filename = extract_filebasename ^ file_delimiter ^ "Opaque" ^ ext in + let opaque_filename = + extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext + in let opaque_module = module_name ^ module_delimiter ^ "Opaque" in let opaque_config = { @@ -1028,13 +1040,18 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : in let clauses_module = if needs_clauses_module then - [ module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"] + let clauses_submodule = + if !Config.backend = Lean then module_delimiter ^ "Clauses" else "" + in + [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ] + else [] + in + let custom_variables = + if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ] else [] in - let custom_variables = if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ] else [] in extract_file fun_config gen_ctx fun_filename crate.A.name fun_module - ": function definitions" [] - ~custom_variables + ": function definitions" [] ~custom_variables ([ types_module ] @ opaque_funs_module @ clauses_module)) else let gen_config = |