summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/ExtractToFStar.ml68
-rw-r--r--src/Pure.ml3
-rw-r--r--src/PureToExtract.ml26
-rw-r--r--src/StringUtils.ml9
-rw-r--r--src/Translate.ml2
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 }