Implement ExtractToFStar.extract_typed_rvalue

5 files changed, 96 insertions, 12 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index fb781939..2f542922 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -65,7 +65,7 @@ let fstar_names_map_init =
  * In Rust:
  *   ```
  *   enum List = {
- *     Cons(u32, Box<List>),
+ *     Cons(u32, Box<List>),x
  *     Nil,
  *   }
  *   ```
@@ -90,7 +90,7 @@ let fstar_names_map_init =
  * up type checking. Note that some languages actually forbids the name clashes
  * (it is the case of F* ).
  *)
-let mk_name_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
+let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
   let int_name (int_ty : integer_type) =
     match int_ty with
     | Isize -> "isize"
@@ -194,6 +194,23 @@ let mk_name_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
   let append_index (basename : string) (i : int) : string =
     basename ^ string_of_int i
   in
+  let extract_constant_value (fmt : F.formatter) (_inside : bool)
+      (cv : constant_value) : unit =
+    match cv with
+    | Scalar sv -> F.pp_print_string fmt (Z.to_string sv.V.value)
+    | Bool b ->
+        let b = if b then "true" else "false" in
+        F.pp_print_string fmt b
+    | Char c -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
+    | String s ->
+        (* We need to replace all the line breaks *)
+        let s =
+          StringUtils.map
+            (fun c -> if c = '\n' then "\n" else String.make 1 c)
+            s
+        in
+        F.pp_print_string fmt ("\"" ^ s ^ "\"")
+  in
   {
     bool_name = "bool";
     char_name = "char";
@@ -207,6 +224,7 @@ let mk_name_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) =
     var_basename;
     type_var_basename;
     append_index;
+    extract_constant_value;
   }
 
 (** [inside] constrols whether we should add parentheses or not around type
@@ -558,10 +576,52 @@ let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter)
       extract_adt_g_value extract_value fmt ctx inside av.variant_id
         av.field_values v.ty
 
+let extract_place (ctx : extraction_ctx) (fmt : F.formatter) (p : place) : unit
+    =
+  let rec extract_projection (pl : projection) : unit =
+    match pl with
+    | [] ->
+        (* No projection element left: print the variable *)
+        let var_name = ctx_get_var p.var ctx in
+        F.pp_print_string fmt var_name
+    | pe :: pl ->
+        (* Extract the interior of the projection *)
+        extract_projection pl;
+        (* Match on the projection element *)
+        let def_id =
+          match pe.pkind with
+          | E.ProjAdt (def_id, None) -> def_id
+          | E.ProjAdt (_, Some _) | E.ProjTuple _ ->
+              (* We can't have field accesses on enumerations (variables for
+               * the fields are introduced upon the moment we match over the
+               * enumeration). We also forbid field access on tuples, because
+               * we don't have the syntax to translate that... We thus
+               * deconstruct the tuples whenever we need to have access:
+               * `let (x, y) = p in ...` *)
+              failwith "Unreachable"
+        in
+        let field_name = ctx_get_field (AdtId def_id) pe.field_id ctx in
+        (* We allow to break where the "." appears *)
+        F.pp_print_break fmt 0 0;
+        F.pp_print_string fmt ".";
+        F.pp_print_string fmt field_name
+  in
+  extract_projection p.projection
+
 (** [inside]: see [extract_ty] *)
 let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (v : typed_rvalue) : unit =
-  raise Unimplemented
+    (inside : bool) (v : typed_rvalue) : extraction_ctx =
+  match v.value with
+  | RvConcrete cv ->
+      ctx.fmt.extract_constant_value fmt inside cv;
+      ctx
+  | RvPlace p ->
+      extract_place ctx fmt p;
+      ctx
+  | RvAdt av ->
+      let extract_value ctx inside v = extract_typed_rvalue ctx fmt inside v in
+      extract_adt_g_value extract_value fmt ctx inside av.variant_id
+        av.field_values v.ty
 
 (** [inside]: see [extract_ty] *)
 let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
diff --git a/src/Pure.ml b/src/Pure.ml
index 32a1ca4c..fd3eb03f 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -134,6 +134,9 @@ type var = {
     itself.
  *)
 
+(* TODO: we might want to redefine field_proj_kind here, to prevent field accesses
+ * on enumerations.
+ * Also: tuples... *)
 type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
 
 type projection = projection_elem list
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 02c507ef..8c8ab76a 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -9,6 +9,7 @@ open Pure
 open TranslateCore
 module C = Contexts
 module RegionVarId = T.RegionVarId
+module F = Format
 
 (** The local logger *)
 let log = L.pure_to_extract_log
@@ -30,7 +31,7 @@ module StringMap = Collections.MakeMap (Collections.OrderedString)
 
 type name = Identifiers.name
 
-type name_formatter = {
+type formatter = {
   bool_name : string;
   char_name : string;
   int_name : integer_type -> string;
@@ -96,17 +97,28 @@ type name_formatter = {
           indices to names, the responsability of finding a proper index is
           delegated to helper functions.
        *)
+  extract_constant_value : F.formatter -> bool -> constant_value -> unit;
+      (** Format a constant value.
+      
+          Inputs:
+          - formatter
+          - [inside]: if `true`, the value should be wrapped in parentheses
+            if it is made of an application (ex.: `U32 3`)
+       *)
 }
-(** A name formatter's role is to come up with name suggestions.
+(** A formatter's role is twofold:
+    1. Come up with name suggestions.
     For instance, provided some information about a function (its basename,
     information about the region group, etc.) it should come up with an
     appropriate name for the forward/backward function.
     
     It can of course apply many transformations, like changing to camel case/
     snake case, adding prefixes/suffixes, etc.
+    
+    2. Format some specific terms, like constants.
  *)
 
-let compute_type_def_name (fmt : name_formatter) (def : type_def) : string =
+let compute_type_def_name (fmt : formatter) (def : type_def) : string =
   fmt.type_name def.name
 
 (** A helper function: generates a function suffix from a region group
@@ -145,14 +157,14 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
         "_back" ^ RegionGroupId.to_string rg.id
 
 (** Extract information from a function, and give this information to a
-    [name_formatter] to generate a function's name.
+    [formatter] to generate a function's name.
     
     Note that we need region information coming from CFIM (when generating
     the name for a backward function, we try to use the names of the regions
     to 
  *)
-let compute_fun_def_name (ctx : trans_ctx) (fmt : name_formatter)
-    (fun_id : A.fun_id) (rg_id : RegionGroupId.id option) : string =
+let compute_fun_def_name (ctx : trans_ctx) (fmt : formatter) (fun_id : A.fun_id)
+    (rg_id : RegionGroupId.id option) : string =
   (* Lookup the function CFIM signature (we need the region information) *)
   let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
   let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in
@@ -297,7 +309,7 @@ let basename_to_unique (names_set : StringSet.t)
 type extraction_ctx = {
   trans_ctx : trans_ctx;
   names_map : names_map;
-  fmt : name_formatter;
+  fmt : formatter;
   indent_incr : int;
       (** The indent increment we insert whenever we need to indent more *)
 }
diff --git a/src/StringUtils.ml b/src/StringUtils.ml
index 2e0e18f7..7c628184 100644
--- a/src/StringUtils.ml
+++ b/src/StringUtils.ml
@@ -86,6 +86,15 @@ let to_snake_case (s : string) : string =
   in
   string_of_chars (List.rev chars)
 
+(** Applies a map operation.
+
+    This is very inefficient, but shouldn't be used much.
+ *)
+let map (f : char -> string) (s : string) : string =
+  let sl = List.map f (string_to_chars s) in
+  let sl = List.map string_to_chars sl in
+  string_of_chars (List.concat sl)
+
 (** Unit tests *)
 let _ =
   assert (to_camel_case "hello_world" = "HelloWorld");
diff --git a/src/Translate.ml b/src/Translate.ml
index efaa43d6..47426c81 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -271,7 +271,7 @@ let translate_module (filename : string) (config : C.partial_config)
   in
   let variant_concatenate_type_name = true in
   let fstar_fmt =
-    ExtractToFStar.mk_name_formatter trans_ctx variant_concatenate_type_name
+    ExtractToFStar.mk_formatter trans_ctx variant_concatenate_type_name
   in
   let extract_ctx =
     { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }