diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Translate.ml | 56 |
1 files changed, 34 insertions, 22 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index c42f3a27..6b3d00f3 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -672,8 +672,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 *) - Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; - Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg; + begin 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; + | 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; (match !Config.backend with | FStar -> Printf.fprintf out "module %s\n" module_name; @@ -700,7 +706,14 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) 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); + Printf.fprintf out "Module %s.\n" module_name + | Lean -> + Printf.fprintf out "import Primitives\nopen result\n\n"; + (* Add the custom imports *) + 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 + ); (* From now onwards, we use the formatter *) (* Set the margin *) Format.pp_set_margin fmt 80; @@ -717,7 +730,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (* Close the module *) (match !Config.backend with - | FStar -> () + | FStar | Lean -> () | Coq -> Printf.fprintf out "End %s .\n" module_name); (* Some logging *) @@ -846,6 +859,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : match !Config.backend with | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst") | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v") + | Config.Lean -> ("/backends/lean/Primitives.lean", "Primitives.lean") in let src = open_in (exe_dir ^ primitives_src) in let tgt_filename = Filename.concat dest_dir primitives_destname in @@ -875,8 +889,9 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : in let module_delimiter = - match !Config.backend with FStar -> "." | Coq -> "_" + match !Config.backend with FStar | Lean -> "." | Coq -> "_" in + let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" in (* Extract one or several files, depending on the configuration *) if !Config.split_files then ( @@ -904,7 +919,8 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : let types_filename_ext = match !Config.backend with | FStar -> if has_opaque_types then ".fsti" else ".fst" - | Coq -> if has_opaque_types then ".v" else ".v" + | Coq -> ".v" + | Lean -> ".lean" in let types_file_suffix = module_delimiter ^ "Types" in let types_filename = @@ -928,24 +944,22 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : !Config.extract_decreases_clauses && not (PureUtils.FunLoopIdSet.is_empty rec_functions) in - (if needs_clauses_module && !Config.extract_template_decreases_clauses then - let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in - let clauses_file_suffix = - module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" - in - let clauses_filename = extract_filebasename ^ clauses_file_suffix ^ ext in - let clauses_module = module_name ^ clauses_file_suffix 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 clauses_file_suffix = + module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" + in + let clauses_filename = extract_filebasename ^ clauses_file_suffix ^ ext in + let clauses_module = module_name ^ clauses_file_suffix 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 ] + []); (* Extract the opaque functions, if needed *) let opaque_funs_module = if has_opaque_funs then ( - let ext = match !Config.backend with FStar -> ".fsti" | Coq -> ".v" in let opaque_file_suffix = module_delimiter ^ "Opaque" in let opaque_filename = extract_filebasename ^ opaque_file_suffix ^ ext in let opaque_module = module_name ^ opaque_file_suffix in @@ -965,7 +979,6 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : in (* Extract the functions *) - let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in let fun_file_suffix = module_delimiter ^ "Funs" in let fun_filename = extract_filebasename ^ fun_file_suffix ^ ext in let fun_module = module_name ^ fun_file_suffix in @@ -1000,7 +1013,6 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : } in (* Add the extension for F* *) - let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" in let extract_filename = extract_filebasename ^ ext in extract_file gen_config gen_ctx extract_filename crate.A.name module_name "" [] [] |