diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0f887ec8..690bff5c 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -665,7 +665,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) let extract_decrease decl = let has_decr_clause = has_decreases_clause decl in if has_decr_clause then - match !Config.backend with + match Config.backend () with | Lean -> Extract.extract_template_lean_termination_and_decreasing ctx fmt decl @@ -864,7 +864,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) * internal count is consistent with the state of the file. *) (* Create the header *) - (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" fi.rust_module_name fi.custom_msg @@ -873,7 +873,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg); (* Generate the imports *) - (match !Config.backend with + (match Config.backend () with | FStar -> Printf.fprintf out "module %s\n" fi.module_name; Printf.fprintf out "open Primitives\n"; @@ -957,7 +957,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Format.pp_print_newline fmt (); (* Close the module *) - (match !Config.backend with + (match Config.backend () with | FStar -> () | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n" @@ -1039,7 +1039,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : trans_ctx; names_maps; indent_incr = 2; - use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses; + use_dep_ite = + Config.backend () = Lean && !Config.extract_decreases_clauses; trait_decl_id = None (* None by default *); is_provided_method = false (* false by default *); trans_trait_decls; @@ -1113,13 +1114,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Convert the case *) let crate_name = StringUtils.to_camel_case basename in let crate_name = - if !Config.backend = HOL4 then + if Config.backend () = HOL4 then 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 + match Config.backend () with | FStar | Coq | HOL4 -> crate.name | Lean -> crate.name in @@ -1144,7 +1145,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Lean reflects the module hierarchy within the filesystem, so we need to create more directories *) - if !Config.backend = Lean then ( + if Config.backend () = Lean then ( let ( ^^ ) = Filename.concat in if !Config.split_files then mkdir_if (dest_dir ^^ crate_name); if needs_clauses_module then ( @@ -1156,7 +1157,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Retrieve the executable's directory *) let exe_dir = Filename.dirname Sys.argv.(0) in let primitives_src_dest = - match !Config.backend with + match Config.backend () with | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst") | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") | Lean -> None @@ -1190,18 +1191,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Extract the file(s) *) let module_delimiter = - match !Config.backend with + match Config.backend () with | FStar -> "." | Coq -> "_" | Lean -> "." | HOL4 -> "_" in let file_delimiter = - if !Config.backend = Lean then "/" else module_delimiter + if Config.backend () = Lean then "/" else module_delimiter in (* File extension for the "regular" modules *) let ext = - match !Config.backend with + match Config.backend () with | FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" @@ -1209,7 +1210,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : in (* File extension for the opaque module *) let opaque_ext = - match !Config.backend with + match Config.backend () with | FStar -> ".fsti" | Coq -> ".v" | Lean -> ".lean" @@ -1253,7 +1254,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : For the other backends, we generate a template file as a model for the file the user has to provide. *) let module_suffix, opaque_imported_suffix, custom_msg = - match !Config.backend with + match Config.backend () with | FStar -> ("TypesExternal", "TypesExternal", ": external type declarations") | HOL4 | Coq | Lean -> @@ -1306,7 +1307,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Extract the non opaque types *) let types_filename_ext = - match !Config.backend with + match Config.backend () with | FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" @@ -1377,7 +1378,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : For the other backends, we generate a template file as a model for the file the user has to provide. *) let module_suffix, opaque_imported_suffix, custom_msg = - match !Config.backend with + match Config.backend () with | FStar -> ( "FunsExternal", "FunsExternal", @@ -1445,7 +1446,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let clauses_module = if needs_clauses_module then let clauses_submodule = - if !Config.backend = Lean then module_delimiter ^ "Clauses" else "" + if Config.backend () = Lean then module_delimiter ^ "Clauses" else "" in [ crate_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ] else [] @@ -1501,7 +1502,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : extract_file gen_config ctx file_info); (* Generate the build file *) - match !Config.backend with + match Config.backend () with | Coq | FStar | HOL4 -> () (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq. |