From fc21cf96f80ccb7e6455c057987bb0ff4597c0bb Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 13 Nov 2022 23:00:38 +0100 Subject: Make good progress on the Coq backend --- compiler/Translate.ml | 224 ++++++++++++++++++++++++++++++++++---------------- 1 file changed, 151 insertions(+), 73 deletions(-) (limited to 'compiler/Translate.ml') diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 79d1c913..b2a28710 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -293,7 +293,7 @@ let translate_module_to_pure (crate : A.crate) : (** Extraction context *) type gen_ctx = { crate : A.crate; - extract_ctx : PureToExtract.extraction_ctx; + extract_ctx : ExtractBase.extraction_ctx; trans_types : Pure.type_decl Pure.TypeDeclId.Map.t; trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t; functions_with_decreases_clause : A.FunDeclId.Set.t; @@ -342,30 +342,41 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool = *) let extract_definitions (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) : unit = - (* Export the definition groups to the file, in the proper order *) - let export_type (qualif : ExtractToBackend.type_decl_qualif) - (id : Pure.TypeDeclId.id) : unit = - (* Retrive the declaration *) + (* Export the definition groups to the file, in the proper order. + - [extract_decl]: extract the type declaration (if not filtered) + - [extract_extra_info]: extra the extra type information (e.g., + the [Arguments] information in Coq). + *) + let export_type (kind : ExtractBase.decl_kind) (id : Pure.TypeDeclId.id) + (extract_decl : bool) (extract_extra_info : bool) : unit = + (* Retrieve the declaration *) let def = Pure.TypeDeclId.Map.find id ctx.trans_types in - (* Update the qualifier, if the type is opaque *) - let is_opaque, qualif = + (* Update the kind, if the type is opaque *) + let is_opaque, kind = match def.kind with - | Enum _ | Struct _ -> (false, qualif) + | Enum _ | Struct _ -> (false, kind) | Opaque -> - let qualif = - if config.interface then ExtractToBackend.TypeVal - else ExtractToBackend.AssumeType + let kind = + if config.interface then ExtractBase.Declared + else ExtractBase.Assumed in - (true, qualif) + (true, kind) in (* Extract, if the config instructs to do so (depending on whether the type * is opaque or not) *) if (is_opaque && config.extract_opaque) || ((not is_opaque) && config.extract_transparent) - then ExtractToBackend.extract_type_decl ctx.extract_ctx fmt qualif def + then ( + if extract_decl then + Extract.extract_type_decl ctx.extract_ctx fmt kind def; + if extract_extra_info then + Extract.extract_type_decl_extra_info ctx.extract_ctx fmt kind def) in + let export_type_decl kind id = export_type kind id true false in + let export_type_extra_info kind id = export_type kind id false true in + (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = A.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause @@ -393,8 +404,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) (fun (_, (fwd, _)) -> let has_decr_clause = has_decreases_clause fwd in if has_decr_clause then - ExtractToBackend.extract_template_decreases_clause ctx.extract_ctx fmt - fwd) + Extract.extract_template_decreases_clause ctx.extract_ctx fmt fwd) pure_ls; (* Extract the function definitions *) (if config.extract_fun_decls then @@ -408,17 +418,25 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) else true else false in + let fls_length = List.length fls in List.iteri (fun i (fwd_def, def) -> let is_opaque = Option.is_none fwd_def.Pure.body in - let qualif = + let kind = if is_opaque then - if config.interface then ExtractToBackend.Val - else ExtractToBackend.AssumeVal - else if not is_rec then ExtractToBackend.Let + if config.interface then ExtractBase.Declared + else ExtractBase.Assumed + else if not is_rec then ExtractBase.SingleNonRec else if is_mut_rec then - if i = 0 then ExtractToBackend.LetRec else ExtractToBackend.And - else ExtractToBackend.LetRec + (* If the functions are mutually recursive, we need to distinguish: + * - the first of the group + * - the last of the group + * - the inner functions + *) + if i = 0 then ExtractBase.MutRecFirst + else if i = fls_length - 1 then ExtractBase.MutRecLast + else ExtractBase.MutRecInner + else ExtractBase.SingleRec in let has_decr_clause = has_decreases_clause def && config.extract_decreases_clauses @@ -428,15 +446,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) then - ExtractToBackend.extract_fun_decl ctx.extract_ctx fmt qualif - has_decr_clause def) + Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause def) fls); (* Insert unit tests if necessary *) if config.test_trans_unit_functions then List.iter (fun (keep_fwd, (fwd, _)) -> if keep_fwd then - ExtractToBackend.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd) + Extract.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd) pure_ls in @@ -454,32 +471,49 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) then - ExtractToBackend.extract_global_decl ctx.extract_ctx fmt global body + Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface in let export_state_type () : unit = - let qualif = - if config.interface then ExtractToBackend.TypeVal - else ExtractToBackend.AssumeType + let kind = + if config.interface then ExtractBase.Declared else ExtractBase.Assumed in - ExtractToBackend.extract_state_type fmt ctx.extract_ctx qualif + Extract.extract_state_type fmt ctx.extract_ctx kind in let export_decl (decl : A.declaration_group) : unit = match decl with | Type (NonRec id) -> - if config.extract_types then export_type ExtractToBackend.Type id + if config.extract_types then ( + let kind = ExtractBase.SingleNonRec in + (* Export the type declaration *) + export_type_decl kind id; + (* Export the extra information (ex.: [Arguments] instructions in Coq) *) + export_type_extra_info kind id) | Type (Rec ids) -> (* Rk.: we shouldn't have (mutually) recursive opaque types *) - if config.extract_types then + let num_decls = List.length ids in + let is_mut_rec = num_decls > 1 in + if config.extract_types then ( + let kind_from_index i = + if not is_mut_rec then ExtractBase.SingleRec + else if i = 0 then ExtractBase.MutRecFirst + else if i = num_decls - 1 then ExtractBase.MutRecLast + else ExtractBase.MutRecInner + in + (* Extract the type declarations *) + List.iteri + (fun i id -> + let kind = kind_from_index i in + export_type_decl kind id) + ids; + (* Export the extra information (ex.: [Arguments] instructions in Coq) *) List.iteri (fun i id -> - let qualif = - if i = 0 then ExtractToBackend.Type else ExtractToBackend.And - in - export_type qualif id) - ids + let kind = kind_from_index i in + export_type_extra_info kind id) + ids) | Fun (NonRec id) -> (* Lookup *) let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in @@ -527,15 +561,33 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (* 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; - Printf.fprintf out "module %s\n" 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; - (* Add the custom includes *) - List.iter (fun m -> Printf.fprintf out "include %s\n" m) 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"; - + (match !Config.backend with + | FStar -> + Printf.fprintf out "module %s\n" 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; + (* Add the custom includes *) + List.iter (fun m -> Printf.fprintf out "include %s\n" m) 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 -> + Printf.fprintf out "Require Import Primitives.\n"; + Printf.fprintf out "Import Primitives.\n"; + Printf.fprintf out "Require Import Coq.ZArith.ZArith.\n"; + Printf.fprintf out "Local Open Scope Primitives_scope.\n"; + + (* Add the custom imports *) + List.iter + (fun m -> Printf.fprintf out "Require Import %s .\n" m) + 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); (* From now onwards, we use the formatter *) (* Set the margin *) Format.pp_set_margin fmt 80; @@ -550,6 +602,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) Format.pp_close_box fmt (); Format.pp_print_newline fmt (); + (* Close the module *) + (match !Config.backend with + | FStar -> () + | Coq -> Printf.fprintf out "End %s .\n" module_name); + (* Some logging *) log#linfo (lazy ("Generated: " ^ filename)); @@ -568,17 +625,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : * We initialize the names map by registering the keywords used in the * language, as well as some primitive names ("u32", etc.) *) let variant_concatenate_type_name = true in - let fstar_fmt = - ExtractToBackend.mk_formatter trans_ctx crate.name + let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in + let fmt, names_map = + mk_formatter_and_names_map trans_ctx crate.name variant_concatenate_type_name in - let names_map = - PureToExtract.initialize_names_map fstar_fmt - ExtractToBackend.fstar_names_map_init - in - let ctx = - { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 } - in + let ctx = { ExtractBase.trans_ctx; names_map; fmt; indent_incr = 2 } in (* We need to compute which functions are recursive, in order to know * whether we should generate a decrease clause or not. *) @@ -596,7 +648,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : * sure there are no name clashes. *) let ctx = List.fold_left - (fun ctx def -> ExtractToBackend.extract_type_decl_register_names ctx def) + (fun ctx def -> Extract.extract_type_decl_register_names ctx def) ctx trans_types in @@ -612,14 +664,13 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : let is_global = (fst def).Pure.is_global_decl_body in if is_global then ctx else - ExtractToBackend.extract_fun_decl_register_names ctx keep_fwd - gen_decr_clause def) + Extract.extract_fun_decl_register_names ctx keep_fwd gen_decr_clause + def) ctx trans_funs in let ctx = - List.fold_left ExtractToBackend.extract_global_decl_register_names ctx - crate.globals + List.fold_left Extract.extract_global_decl_register_names ctx crate.globals in (* Open the output file *) @@ -658,12 +709,17 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : (* Create a directory with *default* permissions *) Core_unix.mkdir_p dest_dir); - (* Copy "Primitives.fst" *) + (* Copy the "Primitives" file *) let _ = (* Retrieve the executable's directory *) let exe_dir = Filename.dirname Sys.argv.(0) in - let src = open_in (exe_dir ^ "/backends/fstar/Primitives.fst") in - let tgt_filename = Filename.concat dest_dir "Primitives.fst" in + let primitives_src, primitives_destname = + match !Config.backend with + | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst") + | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v") + in + let src = open_in (exe_dir ^ primitives_src) in + let tgt_filename = Filename.concat dest_dir primitives_destname in let tgt = open_out tgt_filename in (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *) try @@ -689,6 +745,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : } in + let module_delimiter = + match !Config.backend with FStar -> "." | Coq -> "__" + in + (* Extract one or several files, depending on the configuration *) if !Config.split_files then ( let base_gen_config = @@ -712,9 +772,16 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : (* Extract the types *) (* If there are opaque types, we extract in an interface *) - let types_filename_ext = if has_opaque_types then ".fsti" else ".fst" in - let types_filename = extract_filebasename ^ ".Types" ^ types_filename_ext in - let types_module = module_name ^ ".Types" in + 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" + in + let types_file_suffix = module_delimiter ^ "Types" in + let types_filename = + extract_filebasename ^ types_file_suffix ^ types_filename_ext + in + let types_module = module_name ^ types_file_suffix in let types_config = { base_gen_config with @@ -733,8 +800,12 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : && not (A.FunDeclId.Set.is_empty rec_functions) in (if needs_clauses_module && !Config.extract_template_decreases_clauses then - let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in - let clauses_module = module_name ^ ".Clauses.Template" in + 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 @@ -745,8 +816,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : (* Extract the opaque functions, if needed *) let opaque_funs_module = if has_opaque_funs then ( - let opaque_filename = extract_filebasename ^ ".Opaque.fsti" in - let opaque_module = module_name ^ ".Opaque" in + 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 let opaque_config = { base_gen_config with @@ -763,8 +836,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : in (* Extract the functions *) - let fun_filename = extract_filebasename ^ ".Funs.fst" in - let fun_module = module_name ^ ".Funs" in + 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 let fun_config = { base_gen_config with @@ -773,7 +848,9 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : } in let clauses_module = - if needs_clauses_module then [ module_name ^ ".Clauses" ] else [] + if needs_clauses_module then + [ module_name ^ module_delimiter ^ "Clauses" ] + else [] in extract_file fun_config gen_ctx fun_filename crate.A.name fun_module ": function definitions" [] @@ -794,6 +871,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) : } in (* Add the extension for F* *) - let extract_filename = extract_filebasename ^ ".fst" in + 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 "" [] [] -- cgit v1.2.3