Start generating code for type definitions

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