summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/ExtractToFStar.ml91
-rw-r--r--src/LlbcOfJson.ml1
-rw-r--r--src/Names.ml7
-rw-r--r--src/OfJsonBasic.ml2
-rw-r--r--src/Translate.ml12
5 files changed, 68 insertions, 45 deletions
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 ();
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 93ba7696..19ffc279 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -178,6 +178,7 @@ let type_decl_kind_of_json (js : json) : (T.type_decl_kind, string) result =
| `Assoc [ ("Enum", variants) ] ->
let* variants = list_of_json variant_of_json variants in
Ok (T.Enum variants)
+ | `String "Opaque" -> Ok T.Opaque
| _ -> Error "")
let region_var_group_of_json (js : json) : (T.region_var_group, string) result =
diff --git a/src/Names.ml b/src/Names.ml
index a8e6be59..41177c37 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -53,3 +53,10 @@ type module_name = name [@@deriving show, ord]
type type_name = name [@@deriving show, ord]
type fun_name = name [@@deriving show, ord]
+
+(** Filter the disambiguators equal to 0 in a name *)
+let filter_disambiguators_zero (n : name) : name =
+ let pred (pe : path_elem) : bool =
+ match pe with Ident _ -> true | Disambiguator d -> d <> Disambiguator.zero
+ in
+ List.filter pred n
diff --git a/src/OfJsonBasic.ml b/src/OfJsonBasic.ml
index 6e7bb4e9..9dbd521d 100644
--- a/src/OfJsonBasic.ml
+++ b/src/OfJsonBasic.ml
@@ -11,7 +11,7 @@ let ( let* ) o f = match o with Error e -> Error e | Ok x -> f x
let combine_error_msgs js msg res : ('a, string) result =
match res with
| Ok x -> Ok x
- | Error e -> Error (msg ^ " failed on: " ^ show js ^ "\n" ^ e)
+ | Error e -> Error ("[" ^ msg ^ "]" ^ " failed on: " ^ show js ^ "\n\n" ^ e)
let bool_of_json (js : json) : (bool, string) result =
match js with
diff --git a/src/Translate.ml b/src/Translate.ml
index 5812dc89..a440cacd 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -368,13 +368,17 @@ type gen_config = {
(** Returns the pair: (has opaque type decls, has opaque fun decls) *)
let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
let has_opaque_types =
- T.TypeDeclId.Map.exists
+ Pure.TypeDeclId.Map.exists
(fun _ (d : Pure.type_decl) ->
match d.kind with Opaque -> true | _ -> false)
ctx.trans_types
in
- (* TODO: *)
- let has_opaque_funs = false in
+ let has_opaque_funs =
+ Pure.FunDeclId.Map.exists
+ (fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) ->
+ Option.is_none t_fwd.body)
+ ctx.trans_funs
+ in
(has_opaque_types, has_opaque_funs)
(** A generic utility to generate the extracted definitions: as we may want to
@@ -560,7 +564,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
in
let variant_concatenate_type_name = true in
let fstar_fmt =
- ExtractToFStar.mk_formatter trans_ctx variant_concatenate_type_name
+ ExtractToFStar.mk_formatter trans_ctx m.name variant_concatenate_type_name
in
let ctx =
{ PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:29:03 +0000