diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 39 |
1 files changed, 32 insertions, 7 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 672fb22f..afd3420e 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -692,6 +692,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) | HOL4 -> raise (Failure "HOL4 doesn't have decreases/termination clauses") + | IsabelleHOL -> + raise + (Failure "HOL4 doesn't have decreases/termination clauses") in extract_decrease f.f; List.iter extract_decrease f.loops) @@ -886,7 +889,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) | 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 - | Coq | FStar | HOL4 -> + | Coq | FStar | HOL4 | IsabelleHOL -> Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n"; Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg); @@ -968,7 +971,23 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) 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" fi.module_name); + Printf.fprintf out "val _ = new_theory \"%s\"\n\n" fi.module_name + | IsabelleHOL -> + Printf.fprintf out "theory \"%s\" imports\n" fi.module_name; + (* Add the custom imports and includes *) + let imports = + "Aeneas.Primitives" + :: "HOL-Library.Datatype_Records" + :: 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 ^ "\"") imports in + if imports <> [] then + let imports = String.concat "\n " imports in + Printf.fprintf out " %s\n" imports + else Printf.fprintf out "\n"; + Printf.fprintf out "begin\n\n" + (* Initialize the theory *) + ); (* From now onwards, we use the formatter *) (* Set the margin *) Format.pp_set_margin fmt 80; @@ -988,7 +1007,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) | 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" fi.module_name); + | Coq -> Printf.fprintf out "End %s.\n" fi.module_name + | IsabelleHOL -> Printf.fprintf out "end"); (* Some logging *) if !Errors.error_list <> [] then @@ -1148,7 +1168,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* We use the raw crate name for the namespaces *) let namespace = match Config.backend () with - | FStar | Coq | HOL4 -> crate.name + | FStar | Coq | HOL4 | IsabelleHOL -> crate.name | Lean -> crate.name in (* Concatenate *) @@ -1189,6 +1209,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") | Lean -> None | HOL4 -> None + | IsabelleHOL -> None in match primitives_src_dest with | None -> () @@ -1223,6 +1244,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : | Coq -> "_" | Lean -> "." | HOL4 -> "_" + | IsabelleHOL -> "." in let file_delimiter = if Config.backend () = Lean then "/" else module_delimiter @@ -1234,6 +1256,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : | Coq -> ".v" | Lean -> ".lean" | HOL4 -> "Script.sml" + | IsabelleHOL -> ".thy" in (* File extension for the opaque module *) let opaque_ext = @@ -1242,6 +1265,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : | Coq -> ".v" | Lean -> ".lean" | HOL4 -> "Script.sml" + | IsabelleHOL -> ".thy" in (* Extract one or several files, depending on the configuration *) @@ -1284,7 +1308,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : match Config.backend () with | FStar -> ("TypesExternal", "TypesExternal", ": external type declarations") - | HOL4 | Coq | Lean -> + | HOL4 | Coq | Lean | IsabelleHOL -> ( (* The name of the file we generate *) "TypesExternal_Template", (* The name of the file that will be imported by the Types @@ -1339,6 +1363,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : | Coq -> ".v" | Lean -> ".lean" | HOL4 -> "Script.sml" + | IsabelleHOL -> ".thy" in let types_filename = extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext @@ -1410,7 +1435,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : ( "FunsExternal", "FunsExternal", ": external function declarations" ) - | HOL4 | Coq | Lean -> + | HOL4 | Coq | Lean | IsabelleHOL -> ( (* The name of the file we generate *) "FunsExternal_Template", (* The name of the file that will be imported by the Funs @@ -1530,7 +1555,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : (* Generate the build file *) match Config.backend () with - | Coq | FStar | HOL4 -> + | Coq | FStar | HOL4 | IsabelleHOL -> () (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq. But then we can't modify it if we want to add more files for the proofs |