summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/ExtractToFStar.ml200
-rw-r--r--src/PureToExtract.ml14
2 files changed, 160 insertions, 54 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index e49e7e1a..cd6e7962 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -7,51 +7,155 @@ open PureToExtract
open StringUtils
module F = Format
-(*let mk_name_formatter =
- let int_name (int_ty : integer_type) =
- match int_ty with
- | Isize -> "isize"
- | I8 -> "i8"
- | I16 -> "i16"
- | I32 -> "i32"
- | I64 -> "i64"
- | I128 -> "i128"
- | Usize -> "usize"
- | U8 -> "u8"
- | U16 -> "u16"
- | U32 -> "u32"
- | U64 -> "u64"
- | U128 -> "u128"
- in
- (* For now, we treat only the case where the type name is:
- * `Module::Type`
- * *)
- let type_name name =
- let name = Collections.List.pop_last name in
- to_snake_case name
- in
- let field_name (def_name : name) (field_id : FieldId.id) (field_name : string option) : string =
- let def_name = type_name def_name in
- match field_name with
- | Some field_name -> def_name ^ "_" ^ field_name
- | None -> def_name ^ "_f" ^ FieldId.to_string field_id
- in
- let variant_name (def_name :name) (variant : string) : string =
- type_name def_name ^ to_camel_case variant
- in
- {
- bool_name : "bool";
- char_name : "char";
- int_name;
- str_name : "string";
- field_name;
- variant_name;
- type_name;
- fun_name : A.fun_id -> name -> int -> region_group_info option -> string;
- var_basename : StringSet.t -> ty -> string;
- type_var_basename : StringSet.t -> string;
- append_index : string -> int -> string;
- }*)
+(**
+ * [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
+ * case we use the first letter of the type name.
+ *
+ * [variant_concatenate_type_name]: if true, add the type name as a prefix
+ * to the variant names.
+ * Ex.:
+ * In Rust:
+ * ```
+ * enum List = {
+ * Cons(u32, Box<List>),
+ * Nil,
+ * }
+ * ```
+ *
+ * F*, if option activated:
+ * ```
+ * type list =
+ * | ListCons : u32 -> list -> list
+ * | ListNil : list
+ * ```
+ *
+ * F*, if option not activated:
+ * ```
+ * type list =
+ * | Cons : u32 -> list -> list
+ * | Nil : list
+ * ```
+ *
+ * Rk.: this should be true by default, because in Rust all the variant names
+ * are actively uniquely identifier by the type name `List::Cons(...)`, while
+ * in other languages it is not necessarily the case, and thus clashes can mess
+ * 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 int_name (int_ty : integer_type) =
+ match int_ty with
+ | Isize -> "isize"
+ | I8 -> "i8"
+ | I16 -> "i16"
+ | I32 -> "i32"
+ | I64 -> "i64"
+ | I128 -> "i128"
+ | Usize -> "usize"
+ | U8 -> "u8"
+ | U16 -> "u16"
+ | U32 -> "u32"
+ | U64 -> "u64"
+ | U128 -> "u128"
+ in
+ (* For now, we treat only the case where type and function names are of the
+ * form: `Module::Type` and `Module:function`.
+ *)
+ let get_name (name : name) : string =
+ match name with [ _module; name ] -> name | _ -> failwith "Unexpected"
+ in
+ let type_name_to_camel_case name =
+ let name = get_name name in
+ to_snake_case name
+ in
+ let type_name_to_snake_case name =
+ let name = get_name name in
+ to_snake_case name
+ in
+ let type_name name = type_name_to_camel_case name ^ "_t" in
+ let field_name (def_name : name) (field_id : FieldId.id)
+ (field_name : string option) : string =
+ let def_name = type_name_to_snake_case def_name ^ "_" in
+ match field_name with
+ | Some field_name -> def_name ^ "_" ^ field_name
+ | None -> def_name ^ FieldId.to_string field_id
+ in
+ let variant_name (def_name : name) (variant : string) : string =
+ let variant = to_camel_case variant in
+ if variant_concatenate_type_name then
+ type_name_to_camel_case def_name ^ variant
+ else variant
+ in
+ (* For now, we only treat the case where the type name is:
+ * `Module::Type`
+ *)
+ let fun_name (_fid : A.fun_id) (fname : name) (num_rgs : int)
+ (rg : region_group_info option) : string =
+ let fname = get_name fname in
+ (* Converting to snake case should be a no-op, but it doesn't cost much *)
+ let fname = to_snake_case fname in
+ (* Compute the suffix *)
+ let suffix = default_fun_suffix num_rgs rg in
+ (* Concatenate *)
+ fname ^ suffix
+ in
+ let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
+ : string =
+ (* If there is a basename, we use it *)
+ match basename with
+ | Some basename ->
+ (* This should be a no-op *)
+ to_snake_case basename
+ | None -> (
+ (* No basename: we use the first letter of the type *)
+ match ty with
+ | Adt (type_id, tys) -> (
+ match type_id with
+ | Tuple ->
+ (* The "pair" case is frequent enough to have its special treatment *)
+ if List.length tys = 2 then "p" else "t"
+ | Assumed Result -> "r"
+ | AdtId adt_id ->
+ let def =
+ TypeDefId.Map.find adt_id ctx.type_context.type_defs
+ in
+ StringUtils.string_of_chars [ (get_name def.name).[0] ])
+ | TypeVar _ -> "x" (* lacking imagination here... *)
+ | Bool -> "b"
+ | Char -> "c"
+ | Integer _ -> "i"
+ | Str -> "s"
+ | Array _ | Slice _ -> raise Unimplemented)
+ in
+ let type_var_basename (_varset : StringSet.t) (basename : string option) :
+ string =
+ (* If there is a basename, we use it *)
+ match basename with
+ | Some basename ->
+ (* This is *not* a no-op: type variables in Rust often start with
+ * a capital letter *)
+ to_snake_case basename
+ | None ->
+ (* For no, we use "a" *)
+ "a"
+ in
+ let append_index (basename : string) (i : int) : string =
+ basename ^ string_of_int i
+ in
+ {
+ bool_name = "bool";
+ char_name = "char";
+ int_name;
+ str_name = "string";
+ field_name;
+ variant_name;
+ type_name;
+ fun_name;
+ var_basename;
+ type_var_basename;
+ append_index;
+ }
(** [inside] constrols whether we should add parentheses or not around type
application (if `true` we add parentheses).
@@ -199,7 +303,7 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
in
(* Print the fields *)
let fields = FieldId.mapi (fun fid f -> (fid, f)) variant.fields in
- let ctx =
+ let _ =
List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
in
(* Print the final type *)
@@ -220,8 +324,8 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
(* Close the body box *)
F.pp_close_box fmt ()
-let rec extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
- (def : type_def) : extraction_ctx =
+let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (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:
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index a5619eae..d6e96d3d 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -62,11 +62,12 @@ type name_formatter = {
- region group information in case of a backward function
(`None` if forward function)
*)
- var_basename : StringSet.t -> ty -> string;
+ var_basename : StringSet.t -> string option -> ty -> string;
(** Generates a variable basename.
Inputs:
- the set of names used in the context so far
+ - the basename we got from the symbolic execution, if we have one
- the type of the variable (can be useful for heuristics, in order
not to always use "x" for instance, whenever naming anonymous
variables)
@@ -75,7 +76,7 @@ type name_formatter = {
if necessary to prevent name clashes: the burden of name clashes checks
is thus on the caller's side.
*)
- type_var_basename : StringSet.t -> string;
+ type_var_basename : StringSet.t -> string option -> string;
(** Generates a type variable basename. *)
append_index : string -> int -> string;
(** Appends an index to a name - we use this to generate unique
@@ -104,16 +105,17 @@ let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
: string =
(* There are several cases:
- [rg] is `Some`: this is a forward function:
- - if there are no region groups (i.e., no backward functions) we don't
- add any suffix
- - if there are region gruops, we add "_fwd"
+ - we add "_fwd"
- [rg] is `None`: this is a backward function:
- this function has one region group: we add "_back"
- this function has several backward function: we add "_back" and an
additional suffix to identify the precise backward function
+ Note that we always add a suffix (in case there are no region groups,
+ we could not add the "_fwd" suffix) to prevent name clashes between
+ definitions (in particular between type and function definitions).
*)
match rg with
- | None -> if num_region_groups = 0 then "" else "_fwd"
+ | None -> "_fwd"
| Some rg ->
assert (num_region_groups > 0);
if num_region_groups = 1 then (* Exactly one backward function *)