From 9a080010b0d9ee78a810f8122808f37ea0fc4ee2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Mar 2022 10:39:58 +0100 Subject: Fix minor mistakes with regards to extraction of external declarations --- src/ExtractToFStar.ml | 91 +++++++++++++++++++++++++++++---------------------- 1 file changed, 51 insertions(+), 40 deletions(-) (limited to 'src/ExtractToFStar.ml') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 2e0568c8..2389d444 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -213,26 +213,42 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit) * up type checking. Note that some languages actually forbids the name clashes * (it is the case of F* ). *) -let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : - formatter = +let mk_formatter (ctx : trans_ctx) (crate_name : string) + (variant_concatenate_type_name : bool) : formatter = let int_name = fstar_int_name in - (* For now, we treat only the case where type names are of the - * form: `Module::Type` + (* Prepare a name. + * The first id elem is always the crate: if it is the local crate, + * we remove it. + * We also remove all the disambiguators which are 0, then convert + * everything to strings. *) - let get_type_name (name : name) : string = + let get_name (name : name) : string list = + let name = Names.filter_disambiguators_zero name in match name with - | [ Ident _module; Ident name ] -> name + | Ident crate :: name -> + let name = if crate = crate_name then name else Ident crate :: name in + let name = + List.map + (function + | Names.Ident s -> s + | Disambiguator d -> Names.Disambiguator.to_string d) + name + in + name | _ -> raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) in + let get_type_name = get_name in let type_name_to_camel_case name = let name = get_type_name name in - to_camel_case name + let name = List.map to_camel_case name in + String.concat "" name in let type_name_to_snake_case name = let name = get_type_name name in - to_snake_case name + let name = List.map to_snake_case name in + String.concat "_" name in let type_name name = type_name_to_snake_case name ^ "_t" in let field_name (def_name : name) (field_id : FieldId.id) @@ -252,25 +268,17 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : let tname = type_name basename in "Mk" ^ tname in - (* For now, we treat only the case where function names are of the - * form: - * `module::function` (if top function) - * `module::Type::function` (for implementations) - *) - let get_fun_name (name : fun_name) : string = - match name with - | [ Ident _module_name; Ident name ] -> name - | [ Ident _module_name; Ident ty; Disambiguator _; Ident name ] -> - to_snake_case ty ^ "_" ^ name - | _ -> - raise - (Failure ("Unexpected name shape: " ^ Print.fun_name_to_string name)) + let get_fun_name = get_name in + let fun_name_to_snake_case (fname : fun_name) : string = + let fname = get_fun_name fname in + (* Converting to snake case should be a no-op, but it doesn't cost much *) + let fname = List.map to_snake_case fname in + (* Concatenate the elements *) + String.concat "_" fname in let fun_name (_fid : A.fun_id) (fname : fun_name) (num_rgs : int) (rg : region_group_info option) (filter_info : bool * int) : string = - let fname = get_fun_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 + let fname = fun_name_to_snake_case fname in (* Compute the suffix *) let suffix = default_fun_suffix num_rgs rg filter_info in (* Concatenate *) @@ -278,9 +286,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : in let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string = - let fname = get_fun_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 + let fname = fun_name_to_snake_case fname in (* Compute the suffix *) let suffix = "_decreases" in (* Concatenate *) @@ -311,12 +317,11 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : TypeDeclId.Map.find adt_id ctx.type_context.type_decls in (* We do the following: - * - convert to snake_case + * - compute the type name converted_to_snake_case * - take the first letter of every "letter group" * Ex.: "TypeVar" -> "type_var" -> "tv" *) - let cl = get_type_name def.name in - let cl = StringUtils.to_snake_case cl in + let cl = type_name_to_snake_case def.name in let cl = String.split_on_char '_' cl in let cl = List.filter (fun s -> String.length s > 0) cl in assert (List.length cl > 0); @@ -637,11 +642,16 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "type TYPE_NAME" *) - let is_opaque, qualif = + let is_opaque = + match def.kind with Struct _ | Enum _ -> false | Opaque -> true + in + let qualif = match qualif with - | Type -> (false, "type") - | And -> (false, "and") - | AssumeType -> (true, "assume type") + | Type -> "type" + | And -> "and" + | AssumeType -> + assert is_opaque; + "assume type" in F.pp_print_string fmt (qualif ^ " " ^ def_name); (* Print the type parameters *) @@ -1134,13 +1144,14 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) - let is_opaque, qualif = + let is_opaque = Option.is_none def.body in + let qualif = match qualif with - | Let -> (false, "let") - | LetRec -> (false, "let rec") - | And -> (false, "and") - | Val -> (true, "val") - | AssumeVal -> (true, "AssumeVal") + | Let -> "let" + | LetRec -> "let rec" + | And -> "and" + | Val -> "val" + | AssumeVal -> "AssumeVal" in F.pp_print_string fmt (qualif ^ " " ^ def_name); F.pp_print_space fmt (); -- cgit v1.2.3