From 4f500539e8681c0814cd59fc27680bca73b602c3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 2 Feb 2022 15:48:24 +0100 Subject: Start generating code for type definitions --- src/ExtractToFStar.ml | 50 +++++++++++++++++++++++++++--- src/PureToExtract.ml | 13 ++++++++ src/Translate.ml | 86 +++++++++++++++++++++++++++++++++++++++++++++++++-- src/main.ml | 4 +-- 4 files changed, 144 insertions(+), 9 deletions(-) diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index dcadb773..506b641f 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -7,6 +7,24 @@ open PureToExtract open StringUtils module F = Format +(** A list of keywords/identifiers used in F* and with which we want to check + collision. *) +let fstar_keywords = + [ + "let"; + "rec"; + "in"; + "fn"; + "int"; + "list"; + "FStar"; + "FStar.Mul"; + "type"; + "match"; + "with"; + "assert"; + ] + (** * [ctx]: we use the context to lookup type definitions, to retrieve type names. * This is used to compute variable names, when they have no basenames: in this @@ -328,14 +346,20 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter) (* Close the body box *) F.pp_close_box fmt () -let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def) - : extraction_ctx = +(** Compute the names for all the top-level identifiers used in a type + definition (type name, variant names, field names, etc. but not type + parameters). + + We need to do this preemptively, beforce extracting any definition, + because of recursive definitions. + *) +let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) : + extraction_ctx = (* Compute and register the type def name *) let ctx, def_name = ctx_add_type_def def ctx in (* Compute and register: * - the variant names, if this is an enumeration * - the field names, if this is a structure - * We do this because in F*, they have to be unique at the top-level. *) let ctx = match def.kind with @@ -347,10 +371,24 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def) (VariantId.mapi (fun id v -> (id, v)) variants) ctx) in + (* Return *) + ctx + +(** Extract a type definition. + + Note that all the names used for extraction should already have been + registered. + *) +let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def) + : unit = + (* Retrieve the definition name *) + let def_name = ctx_get_local_type def.def_id ctx in (* Add the type params - note that we remember those bindings only for the * body translation: the updated ctx we return at the end of the function * only contains the registered type def and variant names *) let ctx_body, type_params = ctx_add_type_params def.type_params ctx in + (* Open a box for the definition *) + F.pp_open_hovbox fmt 0; (* > "type TYPE_NAME =" *) F.pp_print_string fmt "type"; F.pp_print_space fmt (); @@ -359,4 +397,8 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def) | Struct fields -> extract_type_def_struct_body ctx_body fmt def fields | Enum variants -> extract_type_def_enum_body ctx_body fmt def def_name type_params variants); - ctx + (* Close the box for the definition *) + F.pp_close_box fmt (); + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0; + F.pp_print_break fmt 0 0 diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index d6e96d3d..4e6c9014 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -211,6 +211,19 @@ type names_map = { We use it for lookups (during the translation) and to check for name clashes. *) +(** Initialize a names map with a proper set of keywords/names coming from the + target language/prover. *) +let initialize_names_map (keywords : string list) : names_map = + let name_to_id = + StringMap.of_list (List.map (fun x -> (x, UnknownId)) keywords) + in + let names_set = StringSet.of_list keywords in + (* We initialize [id_to_name] as empty, because the id of a keyword is [UnknownId]. + * Also note that we don't need this mapping for keywords: we insert keywords only + * to check collisions. *) + let id_to_name = IdMap.empty in + { id_to_name; name_to_id; names_set } + let names_map_add (id : id) (name : string) (nm : names_map) : names_map = (* Sanity check: no clashes *) assert (not (StringSet.mem name nm.names_set)); diff --git a/src/Translate.ml b/src/Translate.ml index dafa2f99..ed9cd22c 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -204,7 +204,7 @@ let translate_function_to_pure (config : C.partial_config) (pure_forward, pure_backwards) let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) : - Pure.type_def list * pure_fun_translation list = + trans_ctx * Pure.type_def list * pure_fun_translation list = (* Debug *) log#ldebug (lazy "translate_module_to_pure"); @@ -257,4 +257,86 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) : in (* Return *) - (type_defs, pure_translations) + (trans_ctx, type_defs, pure_translations) + +(** Translate a module and write the synthesized code to an output file *) +let translate_module (filename : string) (config : C.partial_config) + (m : M.cfim_module) : unit = + (* Translate the module to the pure AST *) + let trans_ctx, trans_types, trans_funs = translate_module_to_pure config m in + + (* Initialize the extraction context - for now we extract only to F* *) + let names_map = + PureToExtract.initialize_names_map ExtractToFStar.fstar_keywords + in + let variant_concatenate_type_name = true in + let fstar_fmt = + ExtractToFStar.mk_name_formatter trans_ctx variant_concatenate_type_name + in + let extract_ctx = + { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 } + in + + (* Register unique names for all the top-level types and functions. + * Note that the order in which we generate the names doesn't matter: + * we just need to generate a mapping from identifier to name, and make + * sure there are no name clashes. *) + let extract_ctx = + List.fold_left + (fun extract_ctx def -> + ExtractToFStar.extract_type_def_register_names extract_ctx def) + extract_ctx trans_types + in + + (* TODO: register the functions *) + + (* Open the output file *) + (* First compute the filename by replacing the extension *) + let filename = + match Filename.chop_suffix_opt ~suffix:".cfim" filename with + | None -> + (* Note that we already checked the suffix upon opening the file *) + failwith "Unreachable" + | Some filename -> + (* We add the extension for F* *) + filename ^ ".fst" + in + let out = open_out filename in + let fmt = Format.formatter_of_out_channel out in + + (* Put the translated definitions in maps *) + let trans_types = + Pure.TypeDefId.Map.of_list + (List.map (fun (d : Pure.type_def) -> (d.def_id, d)) trans_types) + in + let trans_funs = + Pure.FunDefId.Map.of_list + (List.map + (fun ((fd, bdl) : pure_fun_translation) -> (fd.def_id, (fd, bdl))) + trans_funs) + in + + (* Create a vertical box *) + Format.pp_open_vbox fmt 0; + + (* Export the definition groups to the file, in the proper order *) + let export_type (id : Pure.TypeDefId.id) : unit = + let def = Pure.TypeDefId.Map.find id trans_types in + ExtractToFStar.extract_type_def extract_ctx fmt def + in + let export_function (id : Pure.FunDefId.id) : unit = + (* TODO *) + () + in + let export_decl (decl : M.declaration_group) : unit = + match decl with + | Type (NonRec id) -> export_type id + | Type (Rec ids) -> List.iter export_type ids + | Fun (NonRec id) -> export_function id + | Fun (Rec ids) -> List.iter export_function ids + in + List.iter export_decl m.declarations; + + (* Close the box and end the formatting *) + Format.pp_close_box fmt (); + Format.pp_print_newline fmt () diff --git a/src/main.ml b/src/main.ml index e4c4dbd6..c52b7bd3 100644 --- a/src/main.ml +++ b/src/main.ml @@ -86,6 +86,4 @@ let () = I.Test.test_functions_symbolic config synthesize m; (* Translate the functions *) - let _ = Translate.translate_module_to_pure config m in - - () + Translate.translate_module !filename config m -- cgit v1.2.3