From 1fca9c3cc8904198d9b199593554d6517590360a Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 18 Dec 2024 15:35:43 +0100 Subject: [PATCH] wip --- engine/backends/coq/coq/coq_backend.ml | 16 +- .../backends/coq/ssprove/ssprove_backend.ml | 30 +- .../backends/easycrypt/easycrypt_backend.ml | 18 +- engine/backends/fstar/fstar_backend.ml | 101 +- engine/backends/proverif/proverif_backend.ml | 7 +- engine/bin/lib.ml | 2 +- engine/lib/analyses/function_dependency.ml | 5 +- engine/lib/analyses/mutable_variables.ml | 20 +- engine/lib/ast.ml | 2 +- engine/lib/ast_builder.ml | 17 +- engine/lib/ast_utils.ml | 49 +- engine/lib/concrete_ident/concrete_ident.ml | 1203 +++++++++-------- engine/lib/concrete_ident/concrete_ident.mli | 142 +- .../concrete_ident_render_sig.ml | 30 + .../lib/concrete_ident/concrete_ident_sig.ml | 32 - .../concrete_ident/concrete_ident_types.ml | 75 + .../lib/concrete_ident/concrete_ident_view.ml | 202 +++ .../concrete_ident/concrete_ident_view.mli | 4 + .../concrete_ident_view_types.ml | 214 +++ engine/lib/concrete_ident/explicit_def_id.ml | 127 ++ engine/lib/concrete_ident/explicit_def_id.mli | 83 ++ engine/lib/concrete_ident/impl_infos.ml | 2 +- .../lib/concrete_ident/thir_simple_types.ml | 78 ++ engine/lib/dependencies.ml | 242 ++-- .../deprecated_generic_printer.ml | 13 +- .../deprecated_generic_printer.mli | 2 +- engine/lib/dune | 14 + engine/lib/generic_printer/generic_printer.ml | 23 +- engine/lib/import_thir.ml | 163 +-- engine/lib/phases/phase_cf_into_monads.ml | 11 +- engine/lib/phases/phase_direct_and_mut.ml | 3 +- engine/lib/phases/phase_drop_match_guards.ml | 5 +- .../phase_drop_return_break_continue.ml | 2 +- .../lib/phases/phase_functionalize_loops.ml | 12 +- .../lib/phases/phase_reconstruct_asserts.ml | 5 +- .../phase_reconstruct_question_marks.ml | 5 +- .../phases/phase_simplify_question_marks.ml | 17 +- engine/lib/phases/phase_specialize.ml | 2 +- engine/lib/phases/phase_traits_specs.ml | 11 +- engine/lib/print_rust.ml | 46 +- engine/lib/utils.ml | 31 + engine/names/src/lib.rs | 5 +- .../ocaml_of_json_schema.js | 20 +- flake.nix | 3 +- 44 files changed, 1928 insertions(+), 1166 deletions(-) create mode 100644 engine/lib/concrete_ident/concrete_ident_render_sig.ml delete mode 100644 engine/lib/concrete_ident/concrete_ident_sig.ml create mode 100644 engine/lib/concrete_ident/concrete_ident_types.ml create mode 100644 engine/lib/concrete_ident/concrete_ident_view.ml create mode 100644 engine/lib/concrete_ident/concrete_ident_view.mli create mode 100644 engine/lib/concrete_ident/concrete_ident_view_types.ml create mode 100644 engine/lib/concrete_ident/explicit_def_id.ml create mode 100644 engine/lib/concrete_ident/explicit_def_id.mli create mode 100644 engine/lib/concrete_ident/thir_simple_types.ml diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index c4d0426ba..b77e3b411 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -68,7 +68,8 @@ module AST = Ast.Make (InputLanguage) module BackendOptions = Backend.UnitBackendOptions open Ast module CoqNamePolicy = Concrete_ident.DefaultNamePolicy -module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy) +module U = Ast_utils.Make (InputLanguage) +module RenderId = Concrete_ident.MakeRenderAPI (CoqNamePolicy) open AST let hardcoded_coq_headers = @@ -492,7 +493,7 @@ struct let crate = String.capitalize (Option.value ~default:"(TODO CRATE)" - (Option.map ~f:fst current_namespace)) + (Option.bind ~f:List.hd current_namespace)) in let concat_capitalize l = String.concat ~sep:"_" (List.map ~f:String.capitalize l) @@ -509,7 +510,7 @@ struct (crate :: List.drop_last_exn (Option.value ~default:[] - (Option.map ~f:snd current_namespace)) + (Option.bind ~f:List.tl current_namespace)) @ xs) | [ a ] -> a | xs -> concat_capitalize_include xs @@ -729,7 +730,7 @@ struct method concrete_ident ~local:_ id : document = string - (match id.definition with + (match id.name with | "not" -> "negb" | "eq" -> "t_PartialEq_f_eq" | "lt" -> "t_PartialOrd_f_lt" @@ -765,12 +766,13 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list = let my_printer = make m in U.group_items_by_namespace items |> Map.to_alist + |> List.filter_map ~f:(fun (_, items) -> + let* first_item = List.hd items in + Some ((RenderId.render first_item.ident).path, items)) |> List.map ~f:(fun (ns, items) -> let mod_name = String.concat ~sep:"_" - (List.map - ~f:(map_first_letter String.uppercase) - (fst ns :: snd ns)) + (List.map ~f:(map_first_letter String.uppercase) ns) in let sourcemap, contents = let annotated = my_printer#entrypoint_modul items in diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index 8c1870339..cb558f1cd 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -74,7 +74,8 @@ module AST = Ast.Make (InputLanguage) module BackendOptions = Backend.UnitBackendOptions open Ast module CoqNamePolicy = Concrete_ident.DefaultNamePolicy -module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy) +module U = Ast_utils.Make (InputLanguage) +module RenderId = Concrete_ident.MakeRenderAPI (CoqNamePolicy) open AST module SSProveLibrary : Library = struct @@ -553,7 +554,7 @@ end module Context = struct type t = { - current_namespace : string * string list; + current_namespace : string list; analysis_data : StaticAnalysis.analysis_data; } end @@ -617,10 +618,10 @@ module TransformToInputLanguage (* : PHASE *) = (* | None -> Error.unimplemented ~details:err span *) let pconcrete_ident (id : Ast.concrete_ident) : string = - U.Concrete_ident_view.to_definition_name id + (RenderId.render id).name let plocal_ident (e : Local_ident.t) : string = - U.Concrete_ident_view.local_ident + RenderId.local_ident (match String.chop_prefix ~prefix:"impl " e.name with | Some name -> let name = "impl_" ^ Int.to_string ([%hash: string] name) in @@ -689,7 +690,7 @@ struct | Bool b -> SSP.AST.Const_bool b let operators = - let c = Ast.Global_ident.of_name Value in + let c = Ast.Global_ident.of_name ~value:true in [ (c Rust_primitives__hax__array_of_list, (3, [ ""; ".a["; "]<-"; "" ])); (c Core__ops__index__Index__index, (2, [ ""; ".a["; "]" ])); @@ -1555,8 +1556,8 @@ struct let id = [%show: concrete_ident] macro in Error.raise { kind = UnsupportedMacro { id }; span = e.span } in - match U.Concrete_ident_view.to_view macro with - | { crate = "hacspec_lib"; path = _; definition = name } -> ( + match RenderId.render macro with + | { path = "hacspec_lib" :: _; name } -> ( match name with | "public_nat_mod" -> let open Hacspeclib_macro_parser in @@ -1712,7 +1713,7 @@ struct | _ -> unsupported ()) | _ -> unsupported ()) | Use { path; is_external; rename } -> - let _ns_crate, _ns_path = ctx.current_namespace in + let _ns_path = ctx.current_namespace in if is_external then [] else [ SSP.AST.Require (None, (* ns_crate:: ns_path @ *) path, rename) ] @@ -1988,10 +1989,7 @@ let print_item (analysis_data : StaticAnalysis.analysis_data) (item : AST.item) : SSP.AST.decl list = let (module Print) = make - { - current_namespace = U.Concrete_ident_view.to_namespace item.ident; - analysis_data; - } + { current_namespace = (RenderId.render item.ident).path; analysis_data } in Print.pitem item @@ -2421,12 +2419,14 @@ let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list) let analysis_data = StaticAnalysis.analyse items in U.group_items_by_namespace items |> Map.to_alist + |> List.filter_map + ~f: + (snd >> List.hd + >> Option.map ~f:(fun i -> ((RenderId.render i.ident).path, items))) |> List.map ~f:(fun (ns, items) -> let mod_name = String.concat ~sep:"_" - (List.map - ~f:(map_first_letter String.uppercase) - (fst ns :: snd ns)) + (List.map ~f:(map_first_letter String.uppercase) ns) in let file_content = hardcoded_coq_headers ^ "\n" diff --git a/engine/backends/easycrypt/easycrypt_backend.ml b/engine/backends/easycrypt/easycrypt_backend.ml index bf2ed8e6b..d16d9fbd2 100644 --- a/engine/backends/easycrypt/easycrypt_backend.ml +++ b/engine/backends/easycrypt/easycrypt_backend.ml @@ -22,7 +22,8 @@ include module BackendOptions = Backend.UnitBackendOptions module AST = Ast.Make (InputLanguage) module ECNamePolicy = Concrete_ident.DefaultNamePolicy -module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (ECNamePolicy) +module U = Ast_utils.Make (InputLanguage) +module RenderId = Concrete_ident.MakeRenderAPI (ECNamePolicy) open AST module RejectNotEC (FA : Features.T) = struct @@ -88,14 +89,11 @@ module NM = struct { the with subnms = Map.Poly.update ~f:update the.subnms name } - let push_using_namespace (the : nmtree) (nm : string * string list) - (item : AST.item) = - push_using_longname the (List.rev (fst nm :: snd nm)) item + let push_using_namespace (the : nmtree) (nm : string list) (item : AST.item) = + push_using_longname the (List.rev nm) item let push (the : nmtree) (item : AST.item) = - push_using_namespace the - (U.Concrete_ident_view.to_namespace item.ident) - item + push_using_namespace the (RenderId.render item.ident).path item end let suffix_of_size (size : Ast.size) = @@ -132,7 +130,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) : match item.v with | Fn { name; generics; body; params } when List.is_empty generics.params -> - let name = U.Concrete_ident_view.to_definition_name name in + let name = (RenderId.render name).name in doit_fn fmt (name, params, body) | Fn _ -> assert false @@ -166,7 +164,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) : pp_param) params doit_stmt body and doit_concrete_ident (fmt : Formatter.t) (p : Concrete_ident.t) = - Stdlib.Format.fprintf fmt "%s" (U.Concrete_ident_view.to_definition_name p) + Stdlib.Format.fprintf fmt "%s" (RenderId.render p).name and doit_type (fmt : Formatter.t) (typ : ty) = match typ with | TBool -> assert false @@ -281,7 +279,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) : || eq_name Core__cmp__PartialEq__ne op || eq_name Core__cmp__PartialEq__eq op) -> Stdlib.Format.fprintf fmt "(%a) %s (%a)" doit_expr e1 - (match U.Concrete_ident_view.to_definition_name op with + (match (RenderId.render op).name with | "bitxor" -> "^" | "bitand" -> "&" | "bitor" -> "|" diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 7ca56bcb6..5630bdf0a 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -79,19 +79,20 @@ module FStarNamePolicy = struct [@@@ocamlformat "disable"] - let index_field_transform index = "_" ^ index + let anonymous_field_transform index = "_" ^ index let reserved_words = Hash_set.of_list (module String) ["attributes";"noeq";"unopteq";"and";"assert";"assume";"begin";"by";"calc";"class";"default";"decreases";"effect";"eliminate";"else";"end";"ensures";"exception";"exists";"false";"friend";"forall";"fun";"λ";"function";"if";"in";"include";"inline";"inline_for_extraction";"instance";"introduce";"irreducible";"let";"logic";"match";"returns";"as";"module";"new";"new_effect";"layered_effect";"polymonadic_bind";"polymonadic_subcomp";"noextract";"of";"open";"opaque";"private";"quote";"range_of";"rec";"reifiable";"reify";"reflectable";"requires";"set_range_of";"sub_effect";"synth";"then";"total";"true";"try";"type";"unfold";"unfoldable";"val";"when";"with";"_";"__SOURCE_FILE__";"__LINE__";"match";"if";"let";"and";"string"] end -module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (FStarNamePolicy) +module RenderId = Concrete_ident.MakeRenderAPI (FStarNamePolicy) +module U = Ast_utils.Make (InputLanguage) module Visitors = Ast_visitors.Make (InputLanguage) open AST module F = Fstar_ast module Context = struct type t = { - current_namespace : string * string list; + current_namespace : string list; items : item list; interface_mode : bool; line_width : int; @@ -99,9 +100,8 @@ module Context = struct end (** Convers a namespace to a module name *) -let module_name (ns : string * string list) : string = - String.concat ~sep:"." - (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) +let module_name (ns : string list) : string = + String.concat ~sep:"." (List.map ~f:(map_first_letter String.uppercase) ns) module Make (Attrs : Attrs.WITH_ITEMS) @@ -209,11 +209,10 @@ struct | _ -> mk_const @@ pliteral span e let pconcrete_ident (id : concrete_ident) = - let id = U.Concrete_ident_view.to_view id in - let ns_crate, ns_path = ctx.current_namespace in - if String.(ns_crate = id.crate) && [%eq: string list] ns_path id.path then - F.lid [ id.definition ] - else F.lid (id.crate :: (id.path @ [ id.definition ])) + let id = RenderId.render id in + let path = ctx.current_namespace in + if [%eq: string list] path id.path then F.lid [ id.name ] + else F.lid (id.path @ [ id.name ]) let rec pglobal_ident (span : span) (id : global_ident) = match id with @@ -240,7 +239,7 @@ struct ^ show_global_ident id) let plocal_ident_str (e : Local_ident.t) = - U.Concrete_ident_view.local_ident + RenderId.local_ident (match String.chop_prefix ~prefix:"impl " e.name with | Some name -> let name = "impl_" ^ Int.to_string ([%hash: string] name) in @@ -261,8 +260,7 @@ struct ^ show_global_ident f) let index_of_field_concrete id = - try Some (Int.of_string @@ U.Concrete_ident_view.to_definition_name id) - with _ -> None + try Some (Int.of_string @@ (RenderId.render id).name) with _ -> None let index_of_field = function | `Concrete id -> index_of_field_concrete id @@ -272,7 +270,7 @@ struct let is_field_an_index = index_of_field >> Option.is_some let operators = - let c = Global_ident.of_name Value in + let c = Global_ident.of_name ~value:true in [ (c Rust_primitives__hax__array_of_list, (3, ".[]<-")); (c Core__ops__index__Index__index, (2, ".[]")); @@ -342,14 +340,11 @@ struct F.mk_e_app (F.term_of_lid [ "t_Array" ]) [ pty span typ; pexpr length ] | TParam i -> F.term @@ F.AST.Var (F.lid_of_id @@ plocal_ident i) | TAssociatedType { impl = { kind = Self; _ }; item } -> - F.term - @@ F.AST.Var (F.lid [ U.Concrete_ident_view.to_definition_name item ]) + F.term @@ F.AST.Var (F.lid [ (RenderId.render item).name ]) | TAssociatedType { impl; item } -> ( match pimpl_expr span impl with | Some impl -> - F.term - @@ F.AST.Project - (impl, F.lid [ U.Concrete_ident_view.to_definition_name item ]) + F.term @@ F.AST.Project (impl, F.lid [ (RenderId.render item).name ]) | None -> F.term @@ F.AST.Wild) | TOpaque s -> F.term @@ F.AST.Wild | TDyn { goals; _ } -> @@ -554,7 +549,8 @@ struct let body = F.AST.mkConsList F.dummyRange (List.map ~f:pexpr l) in let array_of_list = let id = - Concrete_ident.of_name Value Rust_primitives__hax__array_of_list + Concrete_ident.of_name ~value:true + Rust_primitives__hax__array_of_list in F.term @@ F.AST.Name (pconcrete_ident id) in @@ -921,16 +917,15 @@ struct | Alias { name; item } -> (* These should come from bundled items (in the case of cyclic module dependencies). We make use of this f* feature: https://github.com/FStarLang/FStar/pull/3369 *) - let bundle = U.Concrete_ident_view.to_namespace item |> module_name in + let bundle = (RenderId.render item).path |> module_name in [ `VerbatimImpl ( Printf.sprintf "include %s {%s as %s}" bundle - (U.Concrete_ident_view.to_definition_name item) - (U.Concrete_ident_view.to_definition_name name), + (RenderId.render item).name (RenderId.render name).name, `Newline ); ] | Fn { name; generics; body; params } -> - let name = F.id @@ U.Concrete_ident_view.to_definition_name name in + let name = F.id @@ (RenderId.render name).name in let pat = F.pat @@ F.AST.PatVar (name, None, []) in let generics = FStarBinder.of_generics e.span generics in let pat_args = @@ -962,7 +957,7 @@ struct let name = match pat.p with | PBinding { var; _ } -> - Some (U.Concrete_ident_view.local_ident var) + Some (RenderId.local_ident var) | _ -> (* TODO: this might generate bad code, see @@ -991,9 +986,7 @@ struct else full | TyAlias { name; generics; ty } -> let pat = - F.pat - @@ F.AST.PatVar - (F.id @@ U.Concrete_ident_view.to_definition_name name, None, []) + F.pat @@ F.AST.PatVar (F.id @@ (RenderId.render name).name, None, []) in let ty, quals = (* Adds a refinement if a refinement attribute is detected *) @@ -1031,7 +1024,7 @@ struct F.term @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty) in - let name = F.id @@ U.Concrete_ident_view.to_definition_name name in + let name = F.id @@ (RenderId.render name).name in let erased = erased_impl name arrow_typ [] generics in let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in if ctx.interface_mode then intf :: erased else erased @@ -1048,7 +1041,7 @@ struct false, [ F.AST.TyconRecord - ( F.id @@ U.Concrete_ident_view.to_definition_name name, + ( F.id @@ (RenderId.render name).name, FStarBinder.of_generics e.span generics |> List.map ~f:FStarBinder.implicit_to_explicit |> List.map ~f:FStarBinder.to_binder, @@ -1056,12 +1049,10 @@ struct [], List.map ~f:(fun (prev, (field, ty, attrs)) -> - let fname : string = - U.Concrete_ident_view.to_definition_name field - in + let fname : string = (RenderId.render field).name in let fvars = List.map prev ~f:(fun (field, _, _) -> - U.Concrete_ident_view.to_definition_name field) + (RenderId.render field).name) in ( F.id fname, None, @@ -1072,7 +1063,7 @@ struct | Type { name; generics; variants; _ } -> let self = F.mk_e_app - (F.term_of_lid [ U.Concrete_ident_view.to_definition_name name ]) + (F.term_of_lid [ (RenderId.render name).name ]) (List.map ~f:FStarBinder.(of_generic_param e.span >> to_ident) generics.params @@ -1082,7 +1073,7 @@ struct let constructors = List.map ~f:(fun { name; arguments; is_record; _ } -> - ( F.id (U.Concrete_ident_view.to_definition_name name), + ( F.id (RenderId.render name).name, Some (let field_indexes = List.map ~f:(fst3 >> index_of_field_concrete) arguments @@ -1092,7 +1083,7 @@ struct ( List.map ~f:(fun (field, ty, attrs) -> let fname : string = - U.Concrete_ident_view.to_definition_name field + (RenderId.render field).name in (F.id fname, None, [], pty e.span ty)) arguments, @@ -1115,7 +1106,7 @@ struct false, [ F.AST.TyconVariant - ( F.id @@ U.Concrete_ident_view.to_definition_name name, + ( F.id @@ (RenderId.render name).name, FStarBinder.of_generics e.span generics |> List.map ~f:FStarBinder.implicit_to_explicit |> List.map ~f:FStarBinder.to_binder, @@ -1131,8 +1122,8 @@ struct span = e.span; } in - match U.Concrete_ident_view.to_view macro with - | { crate = "hacspec_lib"; path = _; definition = name } -> ( + match RenderId.render macro with + | { path = "hacspec_lib" :: _; name } -> ( let unwrap r = match r with | Ok r -> r @@ -1194,12 +1185,12 @@ struct | _ -> unsupported_macro ()) | _ -> unsupported_macro ()) | Trait { name; generics; items } -> - let name_str = U.Concrete_ident_view.to_definition_name name in + let name_str = (RenderId.render name).name in let name_id = F.id @@ name_str in let fields = List.concat_map ~f:(fun i -> - let name = U.Concrete_ident_view.to_definition_name i.ti_ident in + let name = (RenderId.render i.ti_ident).name in let generics = FStarBinder.of_generics i.ti_span i.ti_generics in let bds = generics |> List.map ~f:FStarBinder.to_binder in let fields = @@ -1372,8 +1363,9 @@ struct in let add_pre n = n ^ "_pre" in let pre_name_str = - U.Concrete_ident_view.to_definition_name - (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) + (RenderId.render + (Concrete_ident.with_suffix `Pre i.ti_ident)) + .name in let pre = F.mk_app (F.term_of_lid [ pre_name_str ]) inputs @@ -1381,8 +1373,9 @@ struct let result = F.term_of_lid [ "result" ] in let add_post n = n ^ "_post" in let post_name_str = - U.Concrete_ident_view.to_definition_name - (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) + (RenderId.render + (Concrete_ident.with_suffix `Post i.ti_ident)) + .name in let post = F.mk_app @@ -1457,7 +1450,7 @@ struct items; parent_bounds; } -> - let name = U.Concrete_ident_view.to_definition_name e.ident |> F.id in + let name = (RenderId.render e.ident).name |> F.id in let pat = F.pat @@ F.AST.PatVar (name, None, []) in let generics = FStarBinder.of_generics e.span generics in let pat = @@ -1473,7 +1466,7 @@ struct let fields = List.concat_map ~f:(fun { ii_span; ii_generics; ii_v; ii_ident } -> - let name = U.Concrete_ident_view.to_definition_name ii_ident in + let name = (RenderId.render ii_ident).name in match ii_v with | IIFn { body; params } -> @@ -1596,7 +1589,7 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) : let (module Print) = make m { - current_namespace = U.Concrete_ident_view.to_namespace item.ident; + current_namespace = (RenderId.render item.ident).path; interface_mode; items; line_width = bo.line_width; @@ -1638,7 +1631,7 @@ let string_of_items ~mod_name ~bundles (bo : BackendOptions.t) m items : |> Set.union_list (module Concrete_ident) |> Set.map (module String) - ~f:(fun i -> U.Concrete_ident_view.to_namespace i |> module_name) + ~f:(fun i -> (RenderId.render i).path |> module_name) |> Fn.flip Set.remove mod_name |> Set.to_list |> List.filter ~f:(fun m -> @@ -1742,11 +1735,11 @@ let fstar_headers (bo : BackendOptions.t) = (** Translate as F* (the "legacy" printer) *) let translate_as_fstar m (bo : BackendOptions.t) ~(bundles : AST.item list list) (items : AST.item list) : Types.file list = - let show_view Concrete_ident.{ crate; path; definition } = - crate :: (path @ [ definition ]) |> String.concat ~sep:"::" - in U.group_items_by_namespace items |> Map.to_alist + |> List.filter_map ~f:(fun (_, items) -> + let* first_item = List.hd items in + Some ((RenderId.render first_item.ident).path, items)) |> List.concat_map ~f:(fun (ns, items) -> let mod_name = module_name ns in let impl, intf = string_of_items ~mod_name ~bundles bo m items in diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 95778622b..4a1165587 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -98,7 +98,7 @@ module ProVerifNamePolicy = struct [@@@ocamlformat "disable"] - let index_field_transform index = Fn.id index + let anonymous_field_transform index = Fn.id index let reserved_words = Hash_set.of_list (module String) [ "among"; "axiom"; "channel"; "choice"; "clauses"; "const"; "def"; "diff"; "do"; "elimtrue"; "else"; "equation"; "equivalence"; "event"; "expand"; "fail"; "for"; "forall"; "foreach"; "free"; "fun"; "get"; "if"; "implementation"; "in"; "inj-event"; "insert"; "lemma"; "let"; "letfun"; "letproba"; "new"; "noninterf"; "noselect"; "not"; "nounif"; "or"; "otherwise"; "out"; "param"; "phase"; "pred"; "proba"; "process"; "proof"; "public vars"; "putbegin"; "query"; "reduc"; "restriction"; "secret"; "select"; "set"; "suchthat"; "sync"; "table"; "then"; "type"; "weaksecret"; "yield" @@ -111,7 +111,8 @@ module ProVerifNamePolicy = struct let struct_constructor_name_transform constructor_name = constructor_name ^ "_c" end -module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (ProVerifNamePolicy) +module U = Ast_utils.Make (InputLanguage) +module RenderId = Concrete_ident.MakeRenderAPI (ProVerifNamePolicy) open AST module type OPTS = sig @@ -135,7 +136,7 @@ end module Make (Options : OPTS) : MAKE = struct module Print = struct module GenericPrint = - Deprecated_generic_printer.Make (InputLanguage) (U.Concrete_ident_view) + Deprecated_generic_printer.Make (InputLanguage) (RenderId) open Deprecated_generic_printer_base.Make (InputLanguage) open PPrint diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index 71f302bf8..8e13b2c9f 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -27,7 +27,7 @@ let import_thir_items (include_clauses : Types.inclusion_clause list) let imported_items = List.map ~f:(fun item -> - let ident = Concrete_ident.(of_def_id Kind.Value item.owner_id) in + let ident = Concrete_ident.(of_def_id ~value:true item.owner_id) in let most_precise_clause = (* Computes the include clause that apply to `item`, if any *) List.filter diff --git a/engine/lib/analyses/function_dependency.ml b/engine/lib/analyses/function_dependency.ml index 8a42ee869..0bef03ba6 100644 --- a/engine/lib/analyses/function_dependency.ml +++ b/engine/lib/analyses/function_dependency.ml @@ -10,16 +10,13 @@ module%inlined_contents Make (F : Features.T) = struct type analysis_data = concrete_ident list Map.M(String).t type id_order = int - module Uprint = - Ast_utils.MakeWithNamePolicy (F) (Concrete_ident.DefaultNamePolicy) - let analyse (items : A.item list) : analysis_data = let temp_list = List.concat_map ~f:U.functions_of_item items in List.fold_left ~init:(Map.empty (module String)) ~f:(fun y (name, body) -> Map.set y - ~key:(Uprint.Concrete_ident_view.to_definition_name name) + ~key:([%show: Concrete_ident.View.t] (Concrete_ident.to_view name)) ~data: (Set.to_list (U.Reducers.collect_concrete_idents#visit_expr () body))) diff --git a/engine/lib/analyses/mutable_variables.ml b/engine/lib/analyses/mutable_variables.ml index 63e8f5f18..50998ffd9 100644 --- a/engine/lib/analyses/mutable_variables.ml +++ b/engine/lib/analyses/mutable_variables.ml @@ -18,8 +18,7 @@ module%inlined_contents Make (F : Features.T) = struct (* external mut_vars and new variables (e.g. needs def / local) *) Map.M(String).t - module Uprint = - Ast_utils.MakeWithNamePolicy (F) (Concrete_ident.DefaultNamePolicy) + let id_to_string = Concrete_ident.to_view >> [%show: Concrete_ident.View.t] module LocalIdentOrData (Ty : sig type ty [@@deriving compare, sexp] @@ -130,8 +129,7 @@ module%inlined_contents Make (F : Features.T) = struct (module W) (List.map ~f:(fun x -> W.Identifier x) x), m#snd#zero )) - (Map.find data - (Uprint.Concrete_ident_view.to_definition_name cid)) + (Map.find data (id_to_string cid)) | _ -> super#visit_global_ident env x method! visit_concrete_ident (_env : W.t list Map.M(Local_ident).t) @@ -142,8 +140,7 @@ module%inlined_contents Make (F : Features.T) = struct (module W) (List.map ~f:(fun x -> W.Identifier x) x), m#snd#zero )) - (Map.find data - (Uprint.Concrete_ident_view.to_definition_name cid)) + (Map.find data (id_to_string cid)) end) #visit_expr env expr @@ -166,19 +163,14 @@ module%inlined_contents Make (F : Features.T) = struct List.fold_left ~init:(Map.empty (module String (* Concrete_ident *))) ~f:(fun y (x_name, x_items) -> - Map.set y - ~key:(Uprint.Concrete_ident_view.to_definition_name x_name) + Map.set y ~key:(id_to_string x_name) ~data: ( List.map ~f:(fst >> fst) x_items @ Option.value_map ~default:[] ~f: - (List.filter_map - ~f: - (Uprint.Concrete_ident_view.to_definition_name - >> Map.find y) + (List.filter_map ~f:(id_to_string >> Map.find y) >> List.concat_map ~f:fst) - (Map.find func_dep - (Uprint.Concrete_ident_view.to_definition_name x_name)), + (Map.find func_dep (id_to_string x_name)), x_items )) mut_var_list in diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index fbc798cb2..dbdb24aae 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -32,7 +32,7 @@ module Global_ident = struct include M module Map = Map.M (M) - let of_name kind n = `Concrete (Concrete_ident.of_name kind n) + let of_name ~value n = `Concrete (Concrete_ident.of_name ~value n) let eq_name name (x : t) : bool = match x with `Concrete x -> Concrete_ident.eq_name name x | _ -> false diff --git a/engine/lib/ast_builder.ml b/engine/lib/ast_builder.ml index 926fe262b..4a5b01096 100644 --- a/engine/lib/ast_builder.ml +++ b/engine/lib/ast_builder.ml @@ -27,7 +27,9 @@ module Make (F : Features.T) = struct let ty_cf ~(continue_type : ty) ~(break_type : ty) : ty = TApp { - ident = Global_ident.of_name Type Core__ops__control_flow__ControlFlow; + ident = + Global_ident.of_name ~value:false + Core__ops__control_flow__ControlFlow; args = [ GType break_type; GType continue_type ]; } @@ -72,14 +74,13 @@ module Make (F : Features.T) = struct PConstruct { constructor = - Global_ident.of_name - (Constructor { is_struct = false }) + Global_ident.of_name ~value:true Core__ops__control_flow__ControlFlow__Break; fields = [ { field = - Global_ident.of_name Field + Global_ident.of_name ~value:true Core__ops__control_flow__ControlFlow__Break__0; pat; }; @@ -96,14 +97,13 @@ module Make (F : Features.T) = struct PConstruct { constructor = - Global_ident.of_name - (Constructor { is_struct = false }) + Global_ident.of_name ~value:true Core__ops__control_flow__ControlFlow__Continue; fields = [ { field = - Global_ident.of_name Field + Global_ident.of_name ~value:true Core__ops__control_flow__ControlFlow__Continue__0; pat; }; @@ -133,8 +133,7 @@ module Make (F : Features.T) = struct let call_Constructor (constructor_name : Concrete_ident.name) (is_struct : bool) (args : expr list) span ret_typ = call_Constructor' - (`Concrete - (Concrete_ident.of_name (Constructor { is_struct }) constructor_name)) + (`Concrete (Concrete_ident.of_name ~value:true constructor_name)) is_struct args span ret_typ let expr'_Constructor_CF ~(span : span) ~(break_type : ty) diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index 899221e21..ef55bf45c 100644 --- a/engine/lib/ast_utils.ml +++ b/engine/lib/ast_utils.ml @@ -704,7 +704,8 @@ module Make (F : Features.T) = struct let never_typ : ty = let ident = - `Concrete (Concrete_ident.of_name Type Rust_primitives__hax__Never) + `Concrete + (Concrete_ident.of_name ~value:false Rust_primitives__hax__Never) in TApp { ident; args = [] } @@ -900,8 +901,7 @@ module Make (F : Features.T) = struct let call_Constructor (constructor_name : Concrete_ident.name) (is_struct : bool) (args : expr list) span ret_typ = call_Constructor' - (`Concrete - (Concrete_ident.of_name (Constructor { is_struct }) constructor_name)) + (`Concrete (Concrete_ident.of_name ~value:true constructor_name)) is_struct args span ret_typ let call' ?impl f ?(generic_args = []) ?(impl_generic_args = []) @@ -922,11 +922,10 @@ module Make (F : Features.T) = struct span; } - let call ?(kind : Concrete_ident.Kind.t = Value) ?(generic_args = []) - ?(impl_generic_args = []) ?impl (f_name : Concrete_ident.name) - (args : expr list) span ret_typ = + let call ?(generic_args = []) ?(impl_generic_args = []) ?impl + (f_name : Concrete_ident.name) (args : expr list) span ret_typ = call' ?impl ~generic_args ~impl_generic_args - (`Concrete (Concrete_ident.of_name kind f_name)) + (`Concrete (Concrete_ident.of_name ~value:true f_name)) args span ret_typ let make_closure (params : pat list) (body : expr) (span : span) : expr = @@ -951,7 +950,8 @@ module Make (F : Features.T) = struct let hax_failure_typ = let ident = - `Concrete (Concrete_ident.of_name Type Rust_primitives__hax__failure) + `Concrete + (Concrete_ident.of_name ~value:false Rust_primitives__hax__failure) in TApp { ident; args = [] } @@ -1270,37 +1270,14 @@ module Make (F : Features.T) = struct Option.value ~default:p (expect_deref_mut p) end - module StringList = struct - module U = struct - module T = struct - type t = string * string list - [@@deriving show, yojson, compare, sexp, eq, hash] - end - - include T - module C = Base.Comparator.Make (T) - include C - end - - include U - module Map = Map.M (U) - end -end - -module MakeWithNamePolicy (F : Features.T) (NP : Concrete_ident.NAME_POLICY) = -struct - include Make (F) - open AST - module Concrete_ident_view = Concrete_ident.MakeViewAPI (NP) - - let group_items_by_namespace (items : item list) : item list StringList.Map.t - = - let h = Hashtbl.create (module StringList) in + let group_items_by_namespace (items : item list) : + item list Concrete_ident.View.ModPath.Map.t = + let h = Hashtbl.create (module Concrete_ident.View.ModPath) in List.iter items ~f:(fun item -> - let ns = Concrete_ident_view.to_namespace item.ident in + let ns = (Concrete_ident.to_view item.ident).mod_path in let items = Hashtbl.find_or_add h ns ~default:(fun _ -> ref []) in items := !items @ [ item ]); Map.of_iteri_exn - (module StringList) + (module Concrete_ident.View.ModPath) ~iteri:(Hashtbl.map h ~f:( ! ) |> Hashtbl.iteri) end diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index 75505210d..43ddba63b 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -1,579 +1,667 @@ open! Prelude +module View = Concrete_ident_view -module Imported = struct - type def_id = { krate : string; path : path } - and path = disambiguated_def_path_item list +module Fresh_module : sig + (** This module provides a way of generating fresh modules paths. This can be + used to reorganize locally definitions; the main motivation for this is + recursive bundles, where we move definitions from multiple modules to + one fresh module. This is fine because we re-expose all the original + definitions. + *) - and disambiguated_def_path_item = { - data : def_path_item; - disambiguator : int; - } + type t [@@deriving show, yojson, hash, compare, sexp, hash, eq] - and def_path_item = - | CrateRoot - | Impl - | ForeignMod - | Use - | GlobalAsm - | Closure - | Ctor - | AnonConst - | AnonAdt - | OpaqueTy - | TypeNs of string - | ValueNs of string - | MacroNs of string - | LifetimeNs of string - [@@deriving show, yojson, compare, sexp, eq, hash] - - let of_def_path_item : Types.def_path_item -> def_path_item = function - | CrateRoot _ -> CrateRoot - | Impl -> Impl - | ForeignMod -> ForeignMod - | Use -> Use - | GlobalAsm -> GlobalAsm - | Closure -> Closure - | Ctor -> Ctor - | AnonConst -> AnonConst - | OpaqueTy -> OpaqueTy - | TypeNs s -> TypeNs s - | ValueNs s -> ValueNs s - | MacroNs s -> MacroNs s - | LifetimeNs s -> LifetimeNs s - | AnonAdt -> AnonAdt - - let of_disambiguated_def_path_item : - Types.disambiguated_def_path_item -> disambiguated_def_path_item = - fun Types.{ data; disambiguator } -> - { - data = of_def_path_item data; - disambiguator = MyInt64.to_int_exn disambiguator; - } - - let of_def_id - ({ contents = { value = { krate; path; _ }; _ } } : Types.def_id) = - { krate; path = List.map ~f:of_disambiguated_def_path_item path } - - let parent { krate; path; _ } = { krate; path = List.drop_last_exn path } - - let drop_ctor { krate; path; _ } = - { - krate; - path = - (match (List.drop_last path, List.last path) with - | Some path, Some { data = Ctor; _ } -> path - | _ -> path); - } - - let map_def_path_item_string ~(f : string -> string) : - def_path_item -> def_path_item = function - | TypeNs s -> TypeNs (f s) - | ValueNs s -> ValueNs (f s) - | MacroNs s -> MacroNs (f s) - | LifetimeNs s -> LifetimeNs (f s) - | other -> other - - let map_disambiguated_def_path_item_string ~(f : string -> string) - (x : disambiguated_def_path_item) : disambiguated_def_path_item = - { x with data = map_def_path_item_string ~f x.data } - - let map_path_strings ~(f : string -> string) (did : def_id) : def_id = - let f = map_disambiguated_def_path_item_string ~f in - { did with path = List.map ~f did.path } - - module AssociatedItem : sig - type t [@@deriving show, yojson, compare, sexp, eq, hash] - (** An identifier that is an associated item *) - - val from : def_id -> t option - (** If [id] is an associated item [ai], then [from id] evalues to [ai]. *) - - val impl : t -> def_id - (** Lookup the def_id of the [impl] block of an associated item. *) - - val path_decomposition : t -> path * disambiguated_def_path_item * path - (** [some::path::to::Impl#42::assoc::item] is decomposed into [(some::path::to, Impl#42, assoc::item)] *) - end = struct - let is_def_path_item_impl : def_path_item -> bool = function - | Impl -> true - | _ -> false - - (** Cuts a path in two if there is a [Impl] chunk. *) - let decompose_impl_path (path : path) : - (path * disambiguated_def_path_item * path) option = - let l, r = - List.split_while path ~f:(fun x -> is_def_path_item_impl x.data |> not) - in - let* impl_chunk = List.hd r in - let* r = List.tl r in - Some (l, impl_chunk, r) - - type t = { - impl_prefix : def_id; - (** the [def_id] of the impl in which the associated item - lives, but **without** the [Impl] chunk. Do not use this - directly. *) - impl_chunk : disambiguated_def_path_item; (** the [Impl] chunk *) - relative_path : path; - (** the (non-empty) relative path to the associated item *) - } - [@@deriving show, yojson, compare, sexp, eq, hash] - - let from (did : def_id) : t option = - let* impl_prefix, impl_chunk, relative_path = - decompose_impl_path did.path - in - let impl_prefix : def_id = { did with path = impl_prefix } in - if List.is_empty relative_path then None - else Some { impl_prefix; impl_chunk; relative_path } + val fresh : label:string -> Explicit_def_id.t list -> t + (** [fresh ~label hints] creates a fresh module out of the non-empty list of + explicit definition identifiers hints [hints] and out of a label [label]. - let impl { impl_prefix; impl_chunk; _ } = - { impl_prefix with path = impl_prefix.path @ [ impl_chunk ] } + The new module will have a unique path, close to [hints], and containing the + label [label]. + *) - let path_decomposition - { impl_prefix = { path = prefix; _ }; impl_chunk; relative_path } = - (prefix, impl_chunk, relative_path) - end -end + val register : fresh_module:t -> Explicit_def_id.t -> unit + (** [register ~fresh_module id] declares that [id] belongs to [fresh_module]. *) -module ImplInfos = struct - type t = Types.impl_infos - (** Contains the informations [Generics], [Trait] (if not an - inherent type), [Type] and [Bounds] for an [impl] block - [impl [Trait for] Type where Bounds {}] *) -end + val get_path_hints : t -> Explicit_def_id.t list + (** List path hints for a fresh module. *) -(** Stateful store that maps [def_id]s to implementation informations -(which trait is implemented? for which type? under which constraints?) *) -module ImplInfoStore : sig - val init : (Types.def_id * ImplInfos.t) list -> unit - - val find : Imported.def_id -> ImplInfos.t option - (** Given a [id] of type [def_id], [find id] will return [Some - impl_info] when [id] is an (non-inherent[1]) impl. [impl_info] - contains information about the trait being implemented and for - which type. - - [1]: https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations - *) - - val has_impl_prefix : - Imported.def_id -> (ImplInfos.t * Imported.path * Imported.path) option - (** If a [def_id] [did] points to an item that is an [impl] or a - child of an [impl], [has_impl_prefix did] returns [Some (infos, - before, after)]. [infos] is of type [ImplInfos.t] (cf its - documentation). [before] and [after] are the partial paths - before and after the [impl] in [did]'s path. Note that if - [after] is empty, that means [did] points to the [impl] - itself. - - TODO: drop that in favor of [Imported.AssociatedItem] API. - *) + val to_mod_path : t -> View.ModPath.t + (** Compute a module path for a fresh module. *) end = struct - let state : (Imported.def_id, ImplInfos.t) Hashtbl.t option ref = ref None - - module T = struct - type t = Imported.def_id [@@deriving show, yojson, compare, sexp, eq, hash] - end + open View + + type t = { id : int; hints : Explicit_def_id.t list; label : string } + [@@deriving show, yojson, hash, compare, sexp, hash, eq] + + let id_state = ref 0 + let map_state : _ Hashtbl.t = Hashtbl.create (module Int) + + let fresh ~label hints = + id_state := !id_state + 1; + assert (List.is_empty hints |> not); + { id = !id_state; hints; label } + + let register ~(fresh_module : t) (did : Explicit_def_id.t) = + let default = (Set.empty (module ModPath), None) in + let f (set, opt) = (Set.add set (View.of_def_id did).mod_path, opt) in + Hashtbl.update map_state fresh_module.id ~f:(Option.value ~default >> f) + + (** [compute_path_chunks fresh_module] returns [(mod_path, mod_name, + suffixes)]. [suffixes] are optional suffixes to add to [mod_name] so + that the resulting path is unique. *) + let compute_path_chunks (m : t) = + let mod_paths = List.map ~f:(fun d -> (of_def_id d).mod_path) m.hints in + let base = List.longest_prefix ~eq:DisambiguatedString.equal mod_paths in + assert (List.is_empty base |> not); + let module_names = + List.filter ~f:(List.length >> ( < ) (List.length base)) mod_paths + |> List.filter_map ~f:List.last + |> List.dedup_and_sort ~compare:[%compare: DisambiguatedString.t] + in + let hash = + List.dedup_and_sort ~compare:[%compare: Explicit_def_id.t] m.hints + |> [%hash: Explicit_def_id.t list] |> Int.to_string + |> DisambiguatedString.pure + in + let label = DisambiguatedString.pure m.label in + (base, label, module_names @ [ hash ]) - let init impl_infos = - state := - impl_infos - |> List.map ~f:(map_fst Imported.of_def_id) - |> Hashtbl.of_alist_multi (module T) - |> Hashtbl.map ~f:List.hd_exn |> Option.some - - let get_state () = - match !state with - | None -> failwith "ImplInfoStore was not initialized" - | Some state -> state - - let find k = Hashtbl.find (get_state ()) k - - let has_impl_prefix (did : Imported.def_id) = - match Imported.AssociatedItem.from did with - | None -> - let* before = List.tl did.path in - find did |> Option.map ~f:(fun infos -> (infos, before, [])) - | Some assoc_item -> ( - match Imported.AssociatedItem.impl assoc_item |> find with - | Some infos -> - let before, _, after = - Imported.AssociatedItem.path_decomposition assoc_item - in - Some (infos, before, after) - | None -> - (* TODO: This happens in actual code but should not, see #363 and #360. - Make this into an error when #363 is fixed. *) - Logs.warn (fun m -> - m - "concrete_ident: invariant error, no `impl_info` found for \ - identifier `%s`." - ([%show: Imported.def_id] did)); - None) + let all_paths () = + let rust_ones = + Explicit_def_id.State.list_all () + |> List.map ~f:(fun x -> (of_def_id x).mod_path) + in + let fresh_ones : ModPath.t list = + Hashtbl.data map_state |> List.filter_map ~f:snd + in + rust_ones @ fresh_ones + + let compute_path (m : t) = + let mod_path, mod_name, suffixes = compute_path_chunks m in + let existing_names = + all_paths () + |> List.filter_map ~f:last_init + |> List.filter ~f:(fst >> [%eq: ModPath.t] mod_path) + |> List.map ~f:snd + |> List.map ~f:(fun m -> m.DisambiguatedString.data) + |> Set.of_list (module String) + in + let mod_name = + List.mapi ~f:(fun n _ -> mod_name :: List.take suffixes n) suffixes + |> List.map ~f:(List.map ~f:(fun m -> m.DisambiguatedString.data)) + |> List.map ~f:(String.concat ~sep:"_") + |> List.find ~f:(Set.mem existing_names >> not) + |> Option.value_exn + ~message: + "Broken invariant: in fresh modules the suffix is supposed to be \ + crafted so that it is unique." + |> DisambiguatedString.pure + in + mod_path @ [ mod_name ] + + let to_mod_path m = + Hashtbl.update_and_return map_state m.id + ~f: + ( Option.value ~default:(Set.empty (module ModPath), None) + >> fun (paths, alloc) -> + ( paths, + alloc + |> Option.value_or_thunk ~default:(fun () -> compute_path m) + |> Option.some ) ) + |> snd |> Option.value_exn + + let get_path_hints { hints; _ } = hints end -module Kind = struct - type t = - | Type - | Value - | Lifetime - | Constructor of { is_struct : bool } - | Field - | Macro - | Trait - | Impl - | AssociatedItem of t - [@@deriving show, yojson, compare, sexp, eq, hash] - - let of_def_path_item : Imported.def_path_item -> t option = function - | TypeNs _ -> Some Type - | ValueNs _ -> Some Value - | LifetimeNs _ -> Some Lifetime - | _ -> None +type reserved_suffix = [ `Cast | `Pre | `Post ] +[@@deriving show, yojson, hash, compare, sexp, hash, eq] +(** A concrete identifier can have a reserved suffix: this is useful to derive + new identifiers from existing identifiers. *) + +module T = struct + type t = { + def_id : Explicit_def_id.t; + moved : Fresh_module.t option; + suffix : reserved_suffix option; + } + [@@deriving show, yojson, hash, compare, sexp, hash, eq] end -module View = struct - module T = struct - type view = { crate : string; path : string list; definition : string } - end +include T +include Comparator.Make (T) - include T +let to_debug_string = T.show - module Utils = struct - let string_of_def_path_item : Imported.def_path_item -> string option = - function - | TypeNs s | ValueNs s | MacroNs s | LifetimeNs s -> Some s - | Impl -> Some "impl" - | AnonConst -> Some "anon_const" - | _ -> None +let fresh_module ~label = + List.concat_map ~f:(fun { def_id; moved; _ } -> + def_id + :: (Option.to_list moved |> List.concat_map ~f:Fresh_module.get_path_hints)) + >> Fresh_module.fresh ~label - let string_of_disambiguated_def_path_item - (x : Imported.disambiguated_def_path_item) : string option = - let n = x.disambiguator in - string_of_def_path_item x.data - |> Option.map ~f:(fun base -> - match n with - | 0 -> ( - match String.rsplit2 ~on:'_' base with - | Some (_, "") -> base ^ "_" - | Some (_, r) when Option.is_some @@ Stdlib.int_of_string_opt r - -> - base ^ "_" (* potentially conflicting name, adding a `_` *) - | _ -> base) - | _ -> base ^ "_" ^ Int.to_string n) - end +module Cache = struct + let state = Hash_set.create (module T) + let cached = Fn.id &&& Hash_set.add state >> fst +end - open Utils +let make (def_id : Explicit_def_id.t) (moved : Fresh_module.t option) + (suffix : reserved_suffix option) = + { def_id; moved; suffix } + +let of_def_id ?(suffix : reserved_suffix option = None) ~(value : bool) + (def_id : Types.def_id) = + let constructor = + (* A DefId is a constructor when it's a value and points to a variant, a union or a struct. *) + value + && [%matches? (Variant | Union | Struct : Types.def_kind)] + def_id.contents.value.kind + in + make (Explicit_def_id.of_def_id_exn ~constructor def_id) None suffix + |> Cache.cached - let simple_ty_to_string ~(namespace : Imported.def_id) : - Types.node_for__ty_kind -> string option = - let escape = - let re = Re.Pcre.regexp "_((?:e_)*)of_" in - let f group = "_e_" ^ Re.Group.get group 1 ^ "of_" in - Re.replace ~all:true re ~f - in - let adt def_id = - let* () = - [%equal: Imported.def_id] - (Imported.(of_def_id >> parent) def_id) - namespace - |> some_if_true - in - let* last = List.last def_id.contents.value.path in - let* () = some_if_true Int64.(last.disambiguator = zero) in - last.data |> Imported.of_def_path_item |> string_of_def_path_item - |> Option.map ~f:escape - in - let arity0 (ty : Types.node_for__ty_kind) = - match ty.Types.value with - | Bool -> Some "bool" - | Char -> Some "char" - | Str -> Some "str" - | Never -> Some "never" - | Int Isize -> Some "isize" - | Int I8 -> Some "i8" - | Int I16 -> Some "i16" - | Int I32 -> Some "i32" - | Int I64 -> Some "i64" - | Int I128 -> Some "i128" - | Uint Usize -> Some "usize" - | Uint U8 -> Some "u8" - | Uint U16 -> Some "u16" - | Uint U32 -> Some "u32" - | Uint U64 -> Some "u64" - | Uint U128 -> Some "u128" - | Float F32 -> Some "f32" - | Float F64 -> Some "f64" - | Tuple [] -> Some "unit" - | Adt { def_id; generic_args = []; _ } -> - Option.map ~f:escape (adt def_id) - | _ -> None - in - let apply left right = left ^ "_of_" ^ right in - let rec arity1 (ty : Types.node_for__ty_kind) = - match ty.value with - | Slice sub -> arity1 sub |> Option.map ~f:(apply "slice") - | Ref (_, sub, _) -> arity1 sub |> Option.map ~f:(apply "ref") - | Adt { def_id; generic_args = [ Type arg ]; _ } -> - let* adt = adt def_id in - let* arg = arity1 arg in - Some (apply adt arg) - | Tuple l -> - let* l = List.map ~f:arity0 l |> Option.all in - Some ("tuple_" ^ String.concat ~sep:"_" l) - | _ -> arity0 ty - in - arity1 - - let rec to_view (def_id : Imported.def_id) : view = - let impl_infos = ImplInfoStore.has_impl_prefix def_id in - let def_id = - match impl_infos with - (* inherent impl: we don't want the [impl] keyword to appear *) - | Some ({ trait_ref = Some _; _ }, lpath, rpath) - when not (List.is_empty rpath) -> - (* this basically amounts exactly to dropping the [impl] chunk *) - Imported.{ krate = def_id.krate; path = lpath @ rpath } - | _ -> def_id - in - let path, definition = - List.filter_map ~f:string_of_disambiguated_def_path_item def_id.path - |> last_init |> Option.value_exn - in - let path = - List.filter - ~f:(String.is_prefix ~prefix:"hax__autogenerated_refinement__" >> not) - path - in - let sep = "__" in - let subst = String.substr_replace_all ~pattern:sep ~with_:(sep ^ "_") in - let fake_path, real_path = - (* Detects paths of nested items *) - List.rev def_id.path |> List.tl_exn - |> List.split_while ~f:(fun (x : Imported.disambiguated_def_path_item) -> - [%matches? Imported.ValueNs _ | Imported.Impl] x.data) - |> List.rev *** List.rev - in - let subst_dpi = - string_of_disambiguated_def_path_item >> Option.map ~f:subst - in - let definition = subst definition in - let fake_path, definition = - let fake_path' = List.filter_map ~f:subst_dpi fake_path in - match impl_infos with - | Some - ( { trait_ref = None; generics = { params = []; _ }; typ; _ }, - before, - _ ) - when [%matches? [ Imported.{ data = Impl; _ } ]] fake_path -> - let namespace = Imported.{ krate = def_id.krate; path = before } in - simple_ty_to_string ~namespace typ - |> Option.map ~f:(fun typ -> ([ "impl"; typ ], definition)) - |> Option.value ~default:(fake_path', definition) - | Some - ( { - trait_ref = Some { def_id = trait; generic_args = [ _self ] }; - generics = { params = []; _ }; - typ; - _; - }, - before, - [] ) -> - let namespace = Imported.{ krate = def_id.krate; path = before } in - (let* () = - some_if_true - @@ [%equal: Imported.def_id] - (Imported.(of_def_id >> parent) trait) - namespace - in - let* typ = simple_ty_to_string ~namespace typ in - let* trait = List.last trait.contents.value.path in - let* trait = - Imported.of_def_path_item trait.data |> string_of_def_path_item - in - let sep = "_for_" in - let trait = - let re = Re.Pcre.regexp "_((?:e_)*)for_" in - let f group = "_e_" ^ Re.Group.get group 1 ^ "for_" in - Re.replace ~all:true re ~f trait - in - Some ("impl_" ^ trait ^ sep ^ typ)) - |> Option.value ~default:definition - |> tup2 fake_path' - | _ -> (fake_path', definition) - in - let real_path = List.filter_map ~f:subst_dpi real_path in - if List.is_empty fake_path then { crate = def_id.krate; path; definition } - else - let definition = String.concat ~sep (fake_path @ [ definition ]) in - { crate = def_id.krate; path = real_path; definition } +let move_to_fresh_module (fresh_module : Fresh_module.t) (i : t) = + Fresh_module.register ~fresh_module i.def_id; + Cache.cached { i with moved = Some fresh_module } - and to_definition_name x = (to_view x).definition -end +let with_suffix (suffix : reserved_suffix) (i : t) : t = + { i with suffix = Some suffix } -module T = struct - type t = { def_id : Imported.def_id; kind : Kind.t } - [@@deriving show, yojson, sexp] +module type VIEW_RENDERER = sig + val render_module : View.DisambiguatedString.t -> string - (* [kind] is really a metadata, it is not relevant, `def_id`s are unique *) - let equal x y = [%equal: Imported.def_id] x.def_id y.def_id - let compare x y = [%compare: Imported.def_id] x.def_id y.def_id - let of_def_id kind def_id = { def_id = Imported.of_def_id def_id; kind } - let hash x = [%hash: Imported.def_id] x.def_id - let hash_fold_t s x = Imported.hash_fold_def_id s x.def_id + val render_name : + namespace:View.ModPath.t -> View.RelPath.Chunk.t list -> string - type name = Concrete_ident_generated.t - [@@deriving show, yojson, compare, sexp, eq, hash] + val finalize : Concrete_ident_render_sig.rendered -> string +end - let of_name k = Concrete_ident_generated.def_id_of >> of_def_id k +let to_view (ident : t) : Concrete_ident_view.t = + let Concrete_ident_view.{ mod_path; rel_path } = + View.of_def_id ident.def_id + in + let mod_path = + Option.map ~f:Fresh_module.to_mod_path ident.moved + |> Option.value ~default:mod_path + in + { mod_path; rel_path } + +(** Stateful store that maps [def_id]s to implementation informations +(which trait is implemented? for which type? under which constraints?) *) +module ImplInfoStore = struct + include Explicit_def_id.ImplInfoStore + + let lookup_raw (impl : t) : Types.impl_infos option = lookup_raw impl.def_id +end - let eq_name name id = - let of_name = - Concrete_ident_generated.def_id_of name |> Imported.of_def_id +module MakeToString (R : VIEW_RENDERER) = struct + open Concrete_ident_render_sig + + (** For each module namespace, we store three different pieces of data: + - a map from relative paths (i.e. the non-module part of a path) to full + identifiers + - an set of rendered names in this namespace + - a memoization map from full identifiers to rendered names + + If an identifier was already rendered, we just use this already rendered + name. + + Otherwise, when we print a name under a fresh module, we take a look at + the first map: if there is already an identifier in the fresh module with + the exact same relative path, then we have a collision, and we need to + generate a fresh name. + + To generate a fresh name, we use the set of rendered names. + *) + let per_module : + ( string list, + (View.RelPath.t, t) Hashtbl.t + * string Hash_set.t + * (t, string) Hashtbl.t ) + Hashtbl.t = + Hashtbl.create + (module struct + type t = string list [@@deriving hash, compare, sexp, eq] + end) + + let render (i : t) : rendered = + let Concrete_ident_view.{ mod_path; rel_path } = to_view i in + let path = List.map ~f:R.render_module mod_path in + (* Retrieve the various maps. *) + let rel_path_map, name_set, memo = + Hashtbl.find_or_add per_module + ~default:(fun _ -> + ( Hashtbl.create (module View.RelPath), + Hash_set.create (module String), + Hashtbl.create (module T) )) + path + in + (* If we rendered [i] already in the past, just use that. *) + let name = + match Hashtbl.find memo i with + | Some name -> name + | None -> + let name = R.render_name ~namespace:mod_path rel_path in + let name = + match i.suffix with + | Some suffix -> ( + name ^ "_" + ^ + match suffix with + | `Pre -> "pre" + | `Post -> "post" + | `Cast -> "cast_to_repr") + | _ -> name + in + let moved_into_fresh_ns = Option.is_some i.moved in + let name = + if moved_into_fresh_ns then + let escape_sep = + let re = Re.Pcre.regexp "__(e*)from__" in + let f group = "__e" ^ Re.Group.get group 1 ^ "from__" in + Re.replace ~all:true re ~f + in + escape_sep name + else name + in + let name = + match Hashtbl.find rel_path_map rel_path with + | Some _ when moved_into_fresh_ns -> + let path : View.ModPath.t = + (View.of_def_id i.def_id).mod_path + in + let path = List.map ~f:R.render_module path in + (* Generates the list of all prefixes of reversed `path` *) + List.folding_map ~init:[] (List.rev path) ~f:(fun acc chunk -> + let acc = chunk :: acc in + (acc, acc)) + (* We want to try small prefixes first *) + |> List.map ~f:List.rev + (* We generate a fake path with module ancestors *) + |> List.map ~f:(fun path -> + name ^ "__from__" + ^ String.concat ~sep:"__" + path (* This might shadow, we should escape *)) + (* Find the shortest name that doesn't exist already *) + |> List.find ~f:(Hash_set.mem name_set >> not) + |> Option.value_exn + | _ -> name + in + (* Update the maps and hashtables *) + let _ = Hashtbl.add rel_path_map ~key:rel_path ~data:i in + let _ = Hash_set.add name_set name in + let _ = Hashtbl.add memo ~key:i ~data:name in + name in - [%equal: Imported.def_id] of_name id.def_id + { path; name } + + let show (i : t) : string = + let { path; name } = render i in + R.finalize { path; name } end -include T -include View.T -include (val Comparator.make ~compare ~sexp_of_t) +module RenderSig = Concrete_ident_render_sig.Make (T) +include RenderSig -include Concrete_ident_sig.Make (struct - type t_ = t - type view_ = view -end) +module type NAME_POLICY = Concrete_ident_render_sig.NAME_POLICY -module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct - type t = T.t +module MakeRenderAPI (NP : NAME_POLICY) : RENDER_API = struct + open Concrete_ident_render_sig - let pp fmt = show >> Stdlib.Format.pp_print_string fmt let is_reserved_word : string -> bool = Hash_set.mem NP.reserved_words - let rename_definition (_path : string list) (name : string) (kind : Kind.t) - type_name = - (* let path, name = *) - (* match kind with *) - (* | Constructor { is_struct = false } -> *) - (* let path, type_name = (List.drop_last_exn path, List.last_exn path) in *) - (* (path, type_name ^ "_" ^ name) *) - (* | _ -> (path, name) *) - (* in *) - let prefixes = [ "t"; "C"; "v"; "f"; "i"; "discriminant" ] in - let escape s = - match String.lsplit2 ~on:'_' s with - | Some (prefix, _) when List.mem ~equal:String.equal prefixes prefix -> - String.prefix prefix 1 ^ s + module R : VIEW_RENDERER = struct + let disambiguator_escape s = + match split_str ~on:"_" s |> List.rev with + | hd :: _ :: _ when Int.of_string_opt hd |> Option.is_some -> s ^ "_" | _ -> s - in - match kind with - | Type | Trait -> "t_" ^ name - | Value | Impl -> - if start_uppercase name || is_reserved_word name then "v_" ^ name - else escape name - | Constructor { is_struct } -> - let name = - if start_lowercase name || is_reserved_word name then "C_" ^ name - else escape name + + let render_disambiguated View.DisambiguatedString.{ disambiguator; data } = + if Int64.equal Int64.zero disambiguator then disambiguator_escape data + else data ^ "_" ^ Int64.to_string disambiguator + + let render_module = render_disambiguated + + module NameAst = struct + module Separator = struct + let separator = "__" + let concat x y = x ^ separator ^ y + + let escape = + let re = Re.Pcre.regexp "_(e*)_" in + let f group = "_e" ^ Re.Group.get group 1 ^ "_" in + Re.replace ~all:true re ~f + end + + module Prefixes : sig + type t = private string [@@deriving eq, show] + + val allowed : t list + (** List of allowed reserved prefixes. *) + + val mk : string -> t + (** Creates a prefix, if it is valid. *) + + val escape : string -> string + (** Escapes reserved prefixes in a string *) + end = struct + type t = string [@@deriving eq, show] + + let allowed = + [ + "impl"; + "anon_const"; + "foreign"; + "use"; + "opaque"; + "t"; + "C"; + "v"; + "f"; + "i"; + "discriminant"; + ] + + let mem = List.mem ~equal:[%eq: string] allowed + + let mk s = + if mem s then s + else + failwith ("broken invariant: [" ^ s ^ "] is not an allowed prefix") + + let escape_char = "e" + + let () = + assert ( + (* Make sure there is no prefix `Cs` such that `C ^ "s"` is a prefix as well. *) + List.for_all allowed ~f:(fun s -> not (mem (first_letter s ^ s)))) + + let () = assert (mem "e" |> not) + + let rec escape (s : string) : string = + match String.lsplit2 ~on:'_' s with + | Some ("", rest) -> "e_" ^ escape rest + | Some (prefix, rest) + when List.mem ~equal:[%equal: string] allowed prefix -> + first_letter prefix ^ prefix ^ "_" ^ escape rest + | _ -> s + end + + type policy = { + prefix : Prefixes.t; + disable_when : [ `SameCase ] list; + mode : [ `Global | `Local | `Both ]; + } + [@@deriving eq, show] + + type t = + | Concat of (t * t) (** Concatenate two names *) + | Policy of (policy * t) + | TrustedString of string (** A string that is already escaped *) + | UnsafeString of string (** A string that needs escaping *) + | Empty + [@@deriving eq, show] + + let rec global_policy ast : _ = + let filter = + Option.filter ~f:(fun p -> [%matches? `Global | `Both] p.mode) in - if is_struct then NP.struct_constructor_name_transform name - else - let enum_name = type_name |> Option.value_exn in - NP.enum_constructor_name_transform ~enum_name name - | Field | AssociatedItem _ -> - let struct_name = type_name |> Option.value_exn in - NP.field_name_transform ~struct_name - (match Stdlib.int_of_string_opt name with - | Some _ -> NP.index_field_transform name - | _ -> "f_" ^ name) - | Lifetime | Macro -> escape name - - let rec to_view' ({ def_id; kind } : t) : view = - let def_id = Imported.drop_ctor def_id in - let View.{ crate; path; definition } = View.to_view def_id in - let type_name = - try - { def_id = Imported.parent def_id; kind = Type } - |> to_definition_name - |> String.chop_prefix_exn ~prefix:"t_" - |> Option.some - with _ -> None - in - let path, definition = - match kind with - | Constructor { is_struct = false } -> - ( List.drop_last_exn path, - Option.value_exn type_name ^ "_" ^ definition ) - | Field when List.last path |> [%equal: string option] type_name -> - (List.drop_last_exn path, definition) - | AssociatedItem _ -> (List.drop_last_exn path, definition) - | _ -> (path, definition) - in - let definition = rename_definition path definition kind type_name in - View.{ crate; path; definition } - - and to_view ({ def_id; kind } : t) : view = - match List.last def_id.path with - (* Here, we assume an `AnonConst` is a discriminant *) - | Some { data = Imported.AnonConst; _ } -> - let View.{ crate; path; definition } = - to_view' - { - def_id = Imported.parent def_id; - kind = Constructor { is_struct = false }; - } + let ( <|> ) v f = match v with Some v -> Some v | None -> f () in + match ast with + | Policy (policy, contents) -> + global_policy contents |> filter <|> fun _ -> + policy |> Option.some |> filter + | Concat (l, r) -> + global_policy r |> filter <|> fun _ -> global_policy l |> filter + | _ -> None + + let escape_unsafe_string = Prefixes.escape >> Separator.escape + + let apply_policy (leftmost : bool) (policy : policy) (escaped : string) = + let prefix = (policy.prefix :> string) in + let disable = + List.exists policy.disable_when ~f:(function `SameCase -> + let first_upper = first_letter >> is_uppercase in + Bool.equal (first_upper prefix) (first_upper escaped)) + in + if (not disable) || (leftmost && is_reserved_word escaped) then + prefix ^ "_" ^ escaped + else escaped + + let rec norm' = function + | Concat (Empty, x) | Concat (x, Empty) -> x + | Policy (_, Empty) -> Empty + | Policy (p, x) -> Policy (p, norm' x) + | Concat (x, y) -> Concat (norm' x, norm' y) + | x -> x + + let rec norm x = + let x' = norm' x in + if [%eq: t] x x' then x else norm x' + + let concat_list = + List.fold ~f:(fun l r -> Concat (l, r)) ~init:Empty >> norm + + let rec render' leftmost ast = + match ast with + | Concat (a, b) -> + Separator.concat (render' leftmost a) (render' false b) + | Policy (policy, a) when [%matches? `Global] policy.mode -> + render' leftmost a + | Policy (policy, a) -> + render' leftmost a |> apply_policy leftmost policy + | TrustedString s -> s + | UnsafeString s -> escape_unsafe_string s + | Empty -> "" + + let render ast = + let policy = global_policy ast in + let policy = + Option.map ~f:(apply_policy true) policy + |> Option.value ~default:Fn.id in - View.{ crate; path; definition = "discriminant_" ^ definition } - | _ -> to_view' { def_id; kind } + let rendered = norm ast |> render' true |> policy in + if is_reserved_word rendered then rendered ^ "_escape_reserved_word" + else rendered + end + + (** [pretty_impl_name ~namespace impl_infos] computes a pretty impl name given impl informations and a namespace. + A pretty name can be computed when: + - (1) the impl, (2) the type and (3) the trait implemented all live in the same namespace + - the impl block has no generics + - the type implemented is simple enough to be represented as a string (see module {!Thir_simple_types}) + *) + let pretty_impl_name ~namespace (impl_infos : Types.impl_infos) = + let* ty = Thir_simple_types.to_string ~namespace impl_infos.typ in + let*? _no_generics = List.is_empty impl_infos.generics.params in + match impl_infos.trait_ref with + | None -> Some ty + | Some { def_id = trait; generic_args = [ _self ] } -> + let* trait = Explicit_def_id.of_def_id trait in + let trait = View.of_def_id trait in + let*? _same_ns = [%eq: View.ModPath.t] namespace trait.mod_path in + let* trait = + match trait.rel_path with + | [ `Trait (n, _) ] when Int64.equal Int64.zero n.disambiguator -> + Some n.data + | _ -> None + in + let trait = + let re = Re.Pcre.regexp "_((?:e_)*)for_" in + let f group = "_e_" ^ Re.Group.get group 1 ^ "for_" in + Re.replace ~all:true re ~f trait + in + Some (trait ^ "_for_" ^ ty) + | _ -> None - and to_definition_name (x : t) : string = (to_view x).definition + (** Produces a name for an impl block, only if it is necessary (e.g. the disambiguator is non-null) *) + let impl_name ~namespace ?(always = false) disambiguator + (impl_infos : Types.impl_infos option) = + let pretty = impl_infos |> Option.bind ~f:(pretty_impl_name ~namespace) in + let*? _ = always || Int64.equal Int64.zero disambiguator |> not in + match pretty with + | Some pretty -> Some pretty + | None -> + if Int64.equal Int64.zero disambiguator then None + else Some (Int64.to_string disambiguator) + + (** Renders one chunk *) + let rec render_chunk ~namespace (chunk : View.RelPath.Chunk.t) : NameAst.t = + let prefix ?(global = false) ?(disable_when = []) s contents = + NameAst.Policy + ( { + prefix = NameAst.Prefixes.mk s; + mode = (if global then `Both else `Local); + disable_when; + }, + contents ) + in + let prefix_d s d = prefix s (NameAst.UnsafeString (Int64.to_string d)) in + let dstr s = NameAst.UnsafeString (render_disambiguated s) in + let _render_chunk = render_chunk ~namespace in + match chunk with + | `AnonConst d -> prefix_d "anon_const" d + | `Use d -> prefix_d "use" d + | `Foreign d -> prefix_d "foreign" d + | `GlobalAsm d -> prefix_d "global_asm" d + | `Opaque d -> prefix_d "opaque" d + (* The name of a trait impl *) + | `Impl (d, _, impl_infos) -> ( + match impl_name ~namespace d impl_infos with + | Some name -> prefix "impl" (UnsafeString name) + | None -> TrustedString "impl") + (* Print the name of an associated item in a inherent impl *) + | `AssociatedItem + ((`Type n | `Const n | `Fn n), `Impl (d, `Inherent, impl_infos)) -> + let impl = + match impl_name ~always:true ~namespace d impl_infos with + | Some name -> prefix "impl" (UnsafeString name) + | None -> TrustedString "impl" + in + Concat (impl, dstr n) + (* Print the name of an associated item in a trait impl *) + | `AssociatedItem + ((`Type n | `Const n | `Fn n), (`Trait _ | `Impl (_, `Trait, _))) -> + prefix "f" (dstr n) + (* The constructor of a struct *) + | `Constructor (cons, parent) -> + let cons = render_disambiguated cons in + let include_type, type_name = + match parent with + | `Struct n -> (NP.prefix_struct_constructors_with_type, n) + | `Enum n -> (NP.prefix_enum_constructors_with_type, n) + | `Union n -> (NP.prefix_union_constructors_with_type, n) + in + let cons = + if include_type then render_disambiguated type_name ^ "_" ^ cons + else cons + in + prefix ~global:true ~disable_when:[ `SameCase ] "C" + (UnsafeString cons) + (* Anonymous fields *) + | `Field ({ data; disambiguator }, _) + when Option.is_some (Int.of_string_opt data) + && Int64.equal disambiguator Int64.zero -> + UnsafeString (NP.anonymous_field_transform data) + (* Named fields *) + | `Field (n, _) -> prefix "f" (dstr n) + (* Anything function-like *) + | `Macro n | `Static n | `Fn n | `Const n -> + prefix "v" ~disable_when:[ `SameCase ] (dstr n) + (* Anything type-like *) + | `ExternCrate n + | `Trait (n, _) + | `ForeignTy n + | `TraitAlias n + | `Mod n + | `Struct n + | `Union n + | `Enum n -> + prefix "t" (dstr n) + + let render_name ~namespace (rel_path : View.RelPath.t) = + let rel_path = + List.map ~f:(render_chunk ~namespace) rel_path |> NameAst.concat_list + in + NameAst.render rel_path - let to_crate_name (x : t) : string = (to_view x).crate + let finalize { path; name } = + let path = List.map ~f:(map_first_letter String.uppercase) path in + String.concat ~sep:"." + (path @ if String.is_empty name then [] else [ name ]) + end + + include MakeToString (R) - let to_namespace x = - let View.{ crate; path; _ } = to_view x in - (crate, path) + let pp fmt = T.show >> Stdlib.Format.pp_print_string fmt - let show x = - to_view x - |> (fun View.{ crate; path; definition } -> - crate :: (path @ [ definition ])) + let show id = + let { path; name } = render id in + (path @ if String.is_empty name then [] else [ name ]) |> String.concat ~sep:"::" - let local_ident (li : Local_ident.t) = + let local_ident (li : Local_ident.t) : string = if Local_ident.is_final li then li.name else - to_definition_name - { - def_id = - { - krate = "dummy_for_local_name"; - path = [ { data = ValueNs li.name; disambiguator = 0 } ]; - }; - kind = Value; - } + R.render_name ~namespace:[] + [ + `Fn + View.DisambiguatedString. + { disambiguator = Int64.zero; data = li.name }; + ] end -let to_debug_string = T.show +type name = Concrete_ident_generated.t +[@@deriving show, yojson, compare, sexp, eq, hash] -let map_path_strings ~(f : string -> string) (cid : t) : t = - { cid with def_id = Imported.map_path_strings ~f cid.def_id } +let of_name ~value = Concrete_ident_generated.def_id_of >> of_def_id ~value -module DefaultNamePolicy = struct +let eq_name name id = + let of_name = Concrete_ident_generated.def_id_of name in + [%equal: Types.def_id_contents] of_name.contents.value + (Explicit_def_id.to_def_id id.def_id) + +module DefaultNamePolicy : NAME_POLICY = struct let reserved_words = Hash_set.create (module String) - let index_field_transform = Fn.id - let field_name_transform ~struct_name:_ = Fn.id - let enum_constructor_name_transform ~enum_name:_ = Fn.id - let struct_constructor_name_transform = Fn.id + let anonymous_field_transform = Fn.id + let prefix_struct_constructors_with_type = false + let prefix_enum_constructors_with_type = true + let prefix_union_constructors_with_type = false end +module DefaultViewAPI = MakeRenderAPI (DefaultNamePolicy) + +let map_path_strings ~(f : string -> string) (did : t) : t = + let constructor = did.def_id |> Explicit_def_id.is_constructor in + let did : Types.def_id_contents = did.def_id |> Explicit_def_id.to_def_id in + let path = + did.path + |> List.map ~f:(fun (chunk : Types.disambiguated_def_path_item) -> + let data = + match chunk.data with + | TypeNs s -> Types.TypeNs (f s) + | ValueNs s -> ValueNs (f s) + | MacroNs s -> MacroNs (f s) + | LifetimeNs s -> LifetimeNs (f s) + | data -> data + in + { chunk with data }) + in + let did = { did with path } in + let def_id = + Explicit_def_id.of_def_id_exn ~constructor + { contents = { value = did; id = Base.Int64.zero } } + in + { def_id; moved = None; suffix = None } + let matches_namespace (ns : Types.namespace) (did : t) : bool = - let did = did.def_id in + let did = Explicit_def_id.to_def_id did.def_id in let path : string option list = - Some did.krate - :: (did.path - |> List.map ~f:(fun (x : Imported.disambiguated_def_path_item) -> - View.Utils.string_of_def_path_item x.data)) + [ Some did.krate ] + @ List.map + ~f:(fun (chunk : Types.disambiguated_def_path_item) -> + match chunk.data with + | TypeNs s | ValueNs s | MacroNs s | LifetimeNs s -> Some s + | _ -> None) + did.path in let rec aux (pattern : Types.namespace_chunk list) (path : string option list) = @@ -588,72 +676,3 @@ let matches_namespace (ns : Types.namespace) (did : t) : bool = | _ -> false in aux ns.chunks path - -module Create = struct - let parent (id : t) : t = { id with def_id = Imported.parent id.def_id } - - let fresh_module ~from = - let len x = List.length x.def_id.path in - let compare x y = len x - len y in - let id = List.min_elt ~compare from |> Option.value_exn in - { - kind = Kind.Value; - def_id = - { - id.def_id with - path = - id.def_id.path - @ [ - { - data = TypeNs "cyclic_bundle"; - disambiguator = [%hash: t list] from; - }; - ]; - }; - } - - let move_under ~new_parent old = - let new_parent = new_parent.def_id in - { - kind = old.kind; - def_id = - { - new_parent with - path = new_parent.path @ [ List.last_exn old.def_id.path ]; - }; - } - - let map_last ~f old = - let last = - List.last_exn old.def_id.path - |> Imported.map_disambiguated_def_path_item_string ~f - in - let path = List.drop_last_exn old.def_id.path @ [ last ] in - { old with def_id = { old.def_id with path } } - - let constructor name = - let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in - { name with def_id = { name.def_id with path } } - - let add_disambiguator name disambiguator = - let path = name.def_id.path in - if List.is_empty path then name - else - (* The following two `exn` function calls cannot fail as the path is not empty. *) - let last = List.last_exn path in - let path = - List.drop_last_exn path @ [ { data = last.data; disambiguator } ] - in - { name with def_id = { name.def_id with path } } -end - -let lookup_raw_impl_info (impl : t) : Types.impl_infos option = - ImplInfoStore.find impl.def_id - -let parent_impl (id : t) : t option = - let* assoc_item = Imported.AssociatedItem.from id.def_id in - let def_id = Imported.AssociatedItem.impl assoc_item in - Some { def_id; kind = Kind.Impl } - -module DefaultViewAPI = MakeViewAPI (DefaultNamePolicy) -include DefaultViewAPI diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index 545a23da3..21c587206 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/engine/lib/concrete_ident/concrete_ident.mli @@ -1,81 +1,103 @@ -type t [@@deriving show, yojson, compare, sexp, eq, hash] +(** This module provides the global concrete identifiers. *) + +module Fresh_module : sig + type t [@@deriving show, yojson, hash, compare, sexp, hash, eq] + (** A type representing a fresh module. Below, we define two functions: + - [fresh] creates a new fresh module + - [move_to_fresh_module] creates a new and always fresh identifier by + "moving" an existing identifier under the given fresh module + *) +end -type name = Concrete_ident_generated.t -[@@deriving show, yojson, compare, sexp, eq, hash] +module View : module type of Concrete_ident_view -module ImplInfoStore : sig - val init : (Types.def_id * Types.impl_infos) list -> unit +module T : sig + type t [@@deriving show, yojson, compare, sexp, eq, hash] + (** A concrete identifier. *) end -module Kind : sig - type t = - | Type - | Value - | Lifetime - | Constructor of { is_struct : bool } - | Field - | Macro - | Trait - | Impl - | AssociatedItem of t - [@@deriving show, yojson, compare, sexp, eq, hash] -end +include module type of T with type t = T.t -val of_def_id : Kind.t -> Types.def_id -> t -val of_name : Kind.t -> name -> t -val eq_name : name -> t -> bool -val to_debug_string : t -> string +type reserved_suffix = [ `Cast | `Pre | `Post ] +[@@deriving show, yojson, hash, compare, sexp, hash, eq] +(** A concrete identifier can have a reserved suffix: this is useful to derive +new identifiers from existing identifiers. *) -module Create : sig - val parent : t -> t - val fresh_module : from:t list -> t - val move_under : new_parent:t -> t -> t +val of_def_id : + ?suffix:reserved_suffix option -> value:bool -> Types.def_id -> t +(** [of_def_id ?suffix ~value def_id] a concrete identifier out of a Rust +identifier [def_id]. [value] is a flag that decides whether [def_id] +refers to a value or not. - val constructor : t -> t - (** [constructor ident] adds a [Ctor] to [ident] - this allows to build a constructor from a variant name. *) +[value] is important only for constructors: i.e. the identifier for the type +of a struct should be created with [value] set to false while the identifier +for the constructor of a struct should be create with [value] set to true. +For more information, please read the documentation of module +{!Explicit_def_id}. +*) - val map_last : f:(string -> string) -> t -> t - (** [map_last f ident] applies [f] on the last chunk of [ident]'s - path if it holds a string *) +type name = Concrete_ident_generated.t +[@@deriving show, yojson, compare, sexp, eq, hash] +(** A enumeration of static concrete identifiers useful inside the engine. *) - val add_disambiguator : t -> int -> t - (** [add_disambiguator ident d] changes the disambiguator on - the last chunk of [ident]'s path to [d] *) -end +val of_name : value:bool -> name -> t +(** Creates an identifier given a name. [value] has the same meaning as in function {!of_def_id}. *) -type view = { crate : string; path : string list; definition : string } +val eq_name : name -> t -> bool +(** [eq_name name identifier] is true whenever [identifier] is [name]. *) -val map_path_strings : f:(string -> string) -> t -> t -val matches_namespace : Types.namespace -> t -> bool +val to_debug_string : t -> string +(** Format a identifier as a (ppx) debug string. The default debug pretty prints the identifier. *) -include module type of struct - include Concrete_ident_sig.Make (struct - type t_ = t - type view_ = view - end) -end +val fresh_module : label:string -> t list -> Fresh_module.t +(** [fresh_module ~label hints] creates a fresh module given a non-empty list of + existing identifiers and a label. The generated module name will be + unique, will be close to the identifiers found in [hints], and will + include the label. +*) -module MakeViewAPI (NP : NAME_POLICY) : VIEW_API -module DefaultNamePolicy : NAME_POLICY -module DefaultViewAPI : VIEW_API +val move_to_fresh_module : Fresh_module.t -> t -> t +(** Creates a fresh identifier under a given fresh module and given an existing identifier. *) + +val with_suffix : reserved_suffix -> t -> t +(** Creates an identifier out of an existing one, adding a suffix. *) + +val to_view : t -> Concrete_ident_view.t +(** Compute a view for a given identifier. *) + +val map_path_strings : f:(string -> string) -> t -> t +[@@alert unsafe "This function should be only used in Import_thir!"] +(** This function maps any string found in the inner representation of hax. This + is a hack for Import_thir so that we can generically produce identifiers for + any integer type, please do not use it elsewhere. *) type comparator_witness val comparator : (t, comparator_witness) Base.Comparator.comparator -val lookup_raw_impl_info : t -> Types.impl_infos option -(** Lookup the (raw[1]) implementation informations given a concrete -ident. Returns `Some _` if and only if the supplied identifier points -to an `Impl`. +module RenderSig : module type of Concrete_ident_render_sig.Make (T) -[1]: those are raw THIR types. +module type RENDER_API = RenderSig.RENDER_API +module type NAME_POLICY = Concrete_ident_render_sig.NAME_POLICY -{b WARNING}: due to {{: https://github.com/hacspec/hax/issues/363} -issue 363}, when looking up certain identifiers generated by the -engine, this function may return [None] even though the supplied -identifier points to an [Impl] block. *) +module DefaultNamePolicy : NAME_POLICY +module MakeRenderAPI (NP : NAME_POLICY) : RenderSig.RENDER_API +module DefaultViewAPI : RenderSig.RENDER_API + +module ImplInfoStore : sig + val init : (Types.def_id * Types.impl_infos) list -> unit -val parent_impl : t -> t option -(** Returns the identifier pointing to the parent `impl` block, if it -exists. *) + val lookup_raw : t -> Types.impl_infos option + (** Lookup the (raw[1]) implementation informations given a concrete + ident. Returns `Some _` if and only if the supplied identifier points + to an `Impl`. + + [1]: those are raw THIR types. + + {b WARNING}: due to {{: https://github.com/hacspec/hax/issues/363} + issue 363}, when looking up certain identifiers generated by the + engine, this function may return [None] even though the supplied + identifier points to an [Impl] block. *) +end + +val matches_namespace : Types.namespace -> t -> bool diff --git a/engine/lib/concrete_ident/concrete_ident_render_sig.ml b/engine/lib/concrete_ident/concrete_ident_render_sig.ml new file mode 100644 index 000000000..226e3515c --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_render_sig.ml @@ -0,0 +1,30 @@ +open! Prelude + +type rendered = { path : string list; name : string } + +module type NAME_POLICY = sig + val reserved_words : string Hash_set.t + (** List of all words that have a special meaning in the target + language, and that should thus be escaped. *) + + val anonymous_field_transform : string -> string + (** Transformation applied to anonymous tuple fields (i.e. [x.1]) *) + + val prefix_struct_constructors_with_type : bool + val prefix_enum_constructors_with_type : bool + val prefix_union_constructors_with_type : bool +end + +module Make (T : sig + type t +end) = +struct + open T + + module type RENDER_API = sig + val show : t -> string + val pp : Formatter.t -> t -> unit + val render : t -> rendered + val local_ident : Local_ident.t -> string + end +end diff --git a/engine/lib/concrete_ident/concrete_ident_sig.ml b/engine/lib/concrete_ident/concrete_ident_sig.ml deleted file mode 100644 index 09af4797a..000000000 --- a/engine/lib/concrete_ident/concrete_ident_sig.ml +++ /dev/null @@ -1,32 +0,0 @@ -open! Prelude - -module Make (T : sig - type t_ - type view_ -end) = -struct - open T - - module type NAME_POLICY = sig - val reserved_words : string Hash_set.t - (** List of all words that have a special meaning in the target - language, and that should thus be escaped. *) - - val index_field_transform : string -> string - (** Transformation applied to indexes fields name (i.e. [x.1]) *) - - val field_name_transform : struct_name:string -> string -> string - val enum_constructor_name_transform : enum_name:string -> string -> string - val struct_constructor_name_transform : string -> string - end - - module type VIEW_API = sig - val show : t_ -> string - val pp : Formatter.t -> t_ -> unit - val to_view : t_ -> view_ - val to_definition_name : t_ -> string - val to_crate_name : t_ -> string - val to_namespace : t_ -> string * string list - val local_ident : Local_ident.t -> string - end -end diff --git a/engine/lib/concrete_ident/concrete_ident_types.ml b/engine/lib/concrete_ident/concrete_ident_types.ml new file mode 100644 index 000000000..74a34fb69 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_types.ml @@ -0,0 +1,75 @@ +open Prelude + +(** An [ExplicitDefId.t] is a Rust [Types.def_id] tagged with some diambiguation metadata. + + Rust raw [Types.def_id] can be ambiguous: consider the following Rust code: + ```rust + struct S; + fn f() -> S { S } + ``` + Here, the return type of `f` (that is, `S`) and the constructor `S` in the body of `f` refers to the exact same identifier `mycrate::S`. + Yet, they denotes two very different objects: a type versus a constructor. + + [ExplicitDefId.t] clears up this ambiguity, making constructors and types two separate things. + + Also, an [ExplicitDefId.t] always points to an item: an [ExplicitDefId.t] is never pointing to a crate alone. +*) +module type ExplicitDefId = sig + type t [@@deriving show, yojson, hash, compare, sexp, hash, eq] + (** Representation of explicit definition identifiers. *) + + val of_def_id : ?constructor:bool -> Types.def_id -> t option + (** Smart constructor for [t]. + Creates an explicit def id out of a raw Rust definition identifier [Types.def_id]. + + When [of_def_id] is called with [id] a [Types.def_id], if the [kind] of [id] is either [Struct] or [Union], then [constructor] is mandatory. + Otherwise, the argument [constructor] should be [true] only if [id] is a variant. + + This function returns [Some] only when those condition are met. + *) + + val make_exn : ?constructor:bool -> Types.def_id -> t + (** Exception-throwing variant of [make]. + This should be used when we know statically that the conditions + described in the documentation of [make] are met. + + For instance, with static [Types.def_id]s or in [Import_thir]. + *) + + val is_constructor : t -> bool + (** Checks wether a definition identifier [id] points to a constructor. + + [is_constructor id] returns [true] when: + - the kind of [id] is [Struct] or [Union] and the identifier was tagged as a constructor; + - the kind of [id] is [Variant]. + Otherwise, [is_constructor id] returns [false]. + *) + + val parent : t -> t option + (** Looks up the parent of a definition identifier. + Note that the parent of the identifier of a field is always a constructor. + + Also, a top-level item (e.g. `my_crate::some_item`) has no parent: recall that [t] represent only items, not crates. + *) + + val parents : t -> t list + (** Ordered list of parents for an identifier [id], starting with [id], up to the top-most parent identifier. *) + + val to_def_id : t -> Types.def_id_contents + (** Destructor for [t]. *) + + module State : sig + val list_all : unit -> t list + (** List all identifiers the engine dealt with so far. Beware, this function is stateful. *) + end +end + +module ViewTypes = struct + type disambiguator = Int64.t + [@@deriving show, hash, compare, sexp, hash, eq, map] + + module DisambiguatedString = struct + type t = { disambiguator : disambiguator; data : string } + [@@deriving show, hash, compare, sexp, hash, eq, map] + end +end diff --git a/engine/lib/concrete_ident/concrete_ident_view.ml b/engine/lib/concrete_ident/concrete_ident_view.ml new file mode 100644 index 000000000..88b16e879 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_view.ml @@ -0,0 +1,202 @@ +open! Prelude +include Concrete_ident_view_types + +(** Rust paths comes with invariants (e.g. a function is always a `ValueNs _`), this function raises an error if a path doesn't respect those. *) +let broken_invariant (type t) msg (did : Explicit_def_id.t) : t = + let msg = + "Explicit_def_id: an invariant have been broken. Expected " ^ msg + ^ ".\n\ndid=" + ^ [%show: Explicit_def_id.t] did + in + Stdio.prerr_endline msg; + failwith msg + +(** Helper module to asserts various properties about a DefId. *) +module Assert = struct + let parent did = + Explicit_def_id.parent did + |> Option.value_or_thunk ~default:(fun _ -> + broken_invariant "the Explicit_def_id to have a parent" did) + + let type_ns (did : Explicit_def_id.t) = + match List.last (Explicit_def_id.to_def_id did).path with + | Some { data = TypeNs data; disambiguator } -> + DisambiguatedString.{ data; disambiguator } + | _ -> broken_invariant "last path chunk to exist and be of type TypeNs" did + + let macro_ns (did : Explicit_def_id.t) = + match List.last (Explicit_def_id.to_def_id did).path with + | Some { data = MacroNs data; disambiguator } -> + DisambiguatedString.{ data; disambiguator } + | _ -> + broken_invariant "last path chunk to exist and be of type MacroNs" did + + let value_ns (did : Explicit_def_id.t) = + match List.last (Explicit_def_id.to_def_id did).path with + | Some { data = ValueNs data; disambiguator } -> + DisambiguatedString.{ data; disambiguator } + | _ -> + broken_invariant "last path chunk to exist and be of type ValueNs" did +end + +let rec poly : + 'n 'd. + into_n:(Explicit_def_id.t -> DisambiguatedString.t -> 'n) -> + into_d:(Explicit_def_id.t -> Int64.t -> 'd) -> + Explicit_def_id.t -> + ('n, 'd) RelPath.Chunk.poly = + fun ~into_n ~into_d did -> + let poly = poly ~into_n ~into_d in + let mk_associated_item kind : ('n, 'd) RelPath.Chunk.poly = + `AssociatedItem + ( kind, + match Assert.parent did |> poly with + | (`Impl _ | `Trait _) as p -> p + | _ -> broken_invariant "Impl or Trait" (Assert.parent did) ) + in + let assert_type_ns did = Assert.type_ns did |> into_n did in + let assert_value_ns did = Assert.value_ns did |> into_n did in + let assert_macro_ns did = Assert.macro_ns did |> into_n did in + let result = + match (Explicit_def_id.to_def_id did).kind with + | (Ctor (Struct, _) | Struct) when Explicit_def_id.is_constructor did -> + let name = assert_type_ns did in + `Constructor (name, `Struct name) + | Variant | Ctor _ -> + let parent = Assert.parent did in + let name = assert_type_ns did in + `Constructor + ( name, + match poly parent with + | (`Enum _ | `Struct _ | `Union _) as p -> p + | _ -> broken_invariant "Enum, Struct or Union" parent ) + | Fn -> `Fn (assert_value_ns did) + | Const -> `Const (assert_value_ns did) + | AssocFn -> `Fn (assert_value_ns did) |> mk_associated_item + | AssocConst -> `Const (assert_value_ns did) |> mk_associated_item + | AssocTy -> `Type (assert_type_ns did) |> mk_associated_item + | Field -> + let constructor = + let parent = Assert.parent did in + match parent |> poly with + | `Constructor _ as p -> p + | _ -> broken_invariant "Constructor" parent + in + `Field (assert_value_ns did, constructor) + | Trait -> `Trait (assert_type_ns did, None) + | TraitAlias -> `Trait (assert_type_ns did, Some `Alias) + | Macro _ -> `Macro (assert_macro_ns did) + | Union -> `Union (assert_type_ns did) + | Enum -> `Enum (assert_type_ns did) + | Struct -> `Struct (assert_type_ns did) + | AnonConst -> + `AnonConst + (match List.last_exn (Explicit_def_id.to_def_id did).path with + | { data = AnonConst; disambiguator } -> into_d did disambiguator + | _ -> broken_invariant "last path chunk to be AnonConst" did) + | Impl { of_trait } -> + `Impl + (match List.last_exn (Explicit_def_id.to_def_id did).path with + | { data = Impl; disambiguator } -> + ( into_d did disambiguator, + (if of_trait then `Trait else `Inherent), + Explicit_def_id.ImplInfoStore.lookup_raw did ) + | _ -> broken_invariant "last path chunk to be Impl" did) + | OpaqueTy -> + `Opaque + (match List.last_exn (Explicit_def_id.to_def_id did).path with + | { data = OpaqueTy; disambiguator } -> into_d did disambiguator + | _ -> broken_invariant "last path chunk to be Opaque" did) + | Use -> + `Use + (match List.last_exn (Explicit_def_id.to_def_id did).path with + | { data = Use; disambiguator } -> into_d did disambiguator + | _ -> broken_invariant "last path chunk to be Use" did) + | ForeignMod -> + `Foreign + (match List.last_exn (Explicit_def_id.to_def_id did).path with + | { data = ForeignMod; disambiguator } -> into_d did disambiguator + | _ -> broken_invariant "last path chunk to be ForeignMod" did) + | ForeignTy -> `ForeignTy (assert_type_ns did) + | ExternCrate -> `ExternCrate (assert_type_ns did) + | Static _ -> `Static (assert_value_ns did) + | Mod -> `Mod (assert_type_ns did) + | GlobalAsm -> + `GlobalAsm + (match List.last_exn (Explicit_def_id.to_def_id did).path with + | { data = GlobalAsm; disambiguator } -> into_d did disambiguator + | _ -> broken_invariant "last path chunk to be GlobalAsm" did) + | TyAlias | TyParam | ConstParam | InlineConst | LifetimeParam | Closure + | SyntheticCoroutineBody -> + (* It should be impossible for such items to ever be referenced by anyting in hax. *) + broken_invariant + "non (TyAlias | TyParam | ConstParam | InlineConst | LifetimeParam | \ + Closure | SyntheticCoroutineBody) identifier" + did + in + result + +let view_name : Explicit_def_id.t -> RelPath.Chunk.t = + poly ~into_n:(fun _ n -> n) ~into_d:(fun _ d -> d) + +let view_name_did : Explicit_def_id.t -> _ RelPath.Chunk.poly = + let mk x y = (x, y) in + poly ~into_n:mk ~into_d:mk + +let of_def_id (did : Explicit_def_id.t) : t = + (* Decompose the parents of a Explicit_def_id, say `a::b::c::d::e`, into: + - `ns_chunks`, the module parents `[a; a::b]` and into + - `rest`, the remaining parents `[a::b::c; a::b::c::d; a::b::c::d::e]` the rest. *) + (* let ns_chunks, rest = + List.split_while + ~f: + ( Explicit_def_id.to_def_id >> fun def_id -> + match def_id.kind with Mod -> true | _ -> false ) + (Explicit_def_id.parents did |> List.rev) + in *) + (* `rest` is a list of identifiers of items nested each in the others. *) + (* We want to process those items begining with most nested one. *) + (* let rest = List.rev rest in *) + (* We distinguish between: + - a chain of identifiers that have a relation with each other (e.g. if `k::E::C` is a constructor and `k::E` a enum) + - a chain of identifiers that have no relation (e.g. `k::f` and `k::f::g` are both functions). + *) + (* This distinguishing is implemented by `poly` (or `view_name_did` and `view_name`) *) + (* From `poly`, we can inspect the root of the chain of identifiers, e.g. `k::E` is the root of `k::E::C`. *) + let ns_chunks, rel_path = + let rec find name_chunks (did : Explicit_def_id.t) = + let is_mod did = + [%matches? (Types.Mod : Types.def_kind)] + (Explicit_def_id.to_def_id did).kind + in + (let*? _did_is_a_mod = is_mod did in + let parents = Explicit_def_id.parents did in + let*? _parents_all_mods = List.for_all ~f:is_mod parents in + Some (List.rev parents, name_chunks)) + |> Option.value_or_thunk ~default:(fun _ -> + let view = view_name_did did in + let did = + view |> RelPath.Chunk.map_poly fst fst |> RelPath.Chunk.root + in + let name_chunks = + RelPath.Chunk.map_poly snd snd view :: name_chunks + in + match Explicit_def_id.parent did with + | None -> ([], name_chunks) + | Some did -> find name_chunks did) + in + find [] did + in + let mod_path : DisambiguatedString.t list = + { data = (Explicit_def_id.to_def_id did).krate; disambiguator = Int64.zero } + :: List.map + ~f:(fun (m : Explicit_def_id.t) -> + match (Explicit_def_id.to_def_id m).path |> List.last_exn with + | Types.{ disambiguator; data = TypeNs data } -> + DisambiguatedString.{ data; disambiguator } + | _ -> + broken_invariant + "A `Mod` identifier must a `TypeNs` as its last path" m) + ns_chunks + in + { rel_path; mod_path } diff --git a/engine/lib/concrete_ident/concrete_ident_view.mli b/engine/lib/concrete_ident/concrete_ident_view.mli new file mode 100644 index 000000000..2a589f72c --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_view.mli @@ -0,0 +1,4 @@ +include module type of Concrete_ident_view_types + +val of_def_id : Explicit_def_id.t -> t +(** Computes a view for an explicit definition identifier. *) diff --git a/engine/lib/concrete_ident/concrete_ident_view_types.ml b/engine/lib/concrete_ident/concrete_ident_view_types.ml new file mode 100644 index 000000000..3655fc177 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_view_types.ml @@ -0,0 +1,214 @@ +open! Prelude + +(** This modules defines what is the view over a concrete identifiers. + + Hax manipulates concrete identifiers (that is global identifiers refering to + concrete Rust items -- not built-in operators) as raw Rust identifiers + augmented with some metadata. + + Rust represents identifiers as a crate and a path. Each chunk of the path is + roughly a level of nest in Rust. The path lacks informations about + definition kinds. + + There is two kinds of nesting for items. + - Confort: e.g. the user decides to embed a struct within a function to work + with it locally. + - Relational: e.g. an associated method has to be under a trait, or a field + as to be under a constructor. + + This module provides a view to those paths: a path in the view is a list of + smaller relational paths. For instance, consider the following piece of + code: + + {@rust[ + mod a { + impl MyTrait for MyType { + fn assoc_fn() { + struct LocalStruct { + field: u8, + }; + } + } + } + ]} + + Here, the Rust raw definition identifier of [LocalStruct] is roughly + [a::my_crate::::assoc_fn::LocalStruct::field]. + + The view for [LocalStruct] looks like: + [{ + { + path: ["mycrate"; "a"], + name_path: [ + `AssociatedItem ("assoc_fn", `Impl 0); + `Field ("field", `Constructor ("LocalStruct", `Struct "LocalStruct")) + ] + } + }] +*) + +type disambiguator = Int64.t +[@@deriving show, hash, compare, sexp, hash, eq, map] +(** A [Int64.t] disambiguator: this is given by Rust. *) + +(** A string with a disambiguator. *) +module DisambiguatedString = struct + module T = struct + type t = { disambiguator : disambiguator; data : string } + [@@deriving show, hash, compare, sexp, hash, eq, map] + end + + include T + include Base.Comparator.Make (T) + + let pure data = { disambiguator = Int64.zero; data } +end + +(** A "module and crate"-only path. This is the longest `mod` suffix of a + definition identifier path. This is a list of disambiguated strings. *) +module ModPath = struct + module T = struct + open struct + module T = struct + type t = DisambiguatedString.t list + [@@deriving show, hash, compare, sexp, hash, eq] + end + end + + include T + include Base.Comparator.Make (T) + end + + include T + module Map = Map.M (T) +end + +(** A relational path is a path composed of relational chunks. *) +module RelPath = struct + (** A relational chunk is a short path describing "mandatory" nestings between + items: e.g. a field below a struct, an enum below an enum variants, etc. + + The types defined by this module are indexed by two other types: ['name] and + ['disambiguator]. This helps for instrumenting the view to perform + additional operations: see [collect_either], [collect] and [root]. + *) + module Chunk = struct + type 'name type_definition = + [ `Enum of 'name | `Struct of 'name | `Union of 'name ] + (** A type can be an enum, a struct or a union. A type is standalone: it has no mandatory parent item. *) + + and 'name constructor = [ `Constructor of 'name * 'name type_definition ] + (** A constructor always has a parent type definition. *) + + and 'name maybe_associated = [ `Fn of 'name | `Const of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, map] + (** Helper type for function and constants: those exists both as associated + in an impl block or a trait, and as standalone. *) + + type 'name associated = [ 'name maybe_associated | `Type of 'name ] + (** An associated item. This is pulled out of [`AssociatedItem] below: + otherwise, some PPX is broken... *) + + and ('name, 'disambiguator) assoc_parent = + [ `Impl of + 'disambiguator * [ `Inherent | `Trait ] * Types.impl_infos option + | `Trait of 'name * [ `Alias ] option ] + [@@deriving show, hash, compare, sexp, hash, eq, map] + (** The parent of an associated item can be an impl or a trait. *) + + type ('name, 'disambiguator) poly = + [ 'name type_definition + | 'name constructor + | 'name maybe_associated + | ('name, 'disambiguator) assoc_parent + | `Use of 'disambiguator + | `AnonConst of 'disambiguator + | `TraitAlias of 'name + | `Foreign of 'disambiguator + | `ForeignTy of 'name + | `ExternCrate of 'name + | `Opaque of 'disambiguator + (** This is e.g.: {[ + fn f() -> impl Clone {} + fn g() { + f(); + } + ]} + Here, the type of `f()` is ``. + *) + | `Static of 'name + | `Macro of 'name + | `AssociatedItem of + 'name associated * ('name, 'disambiguator) assoc_parent + | `Mod of 'name + | `GlobalAsm of 'disambiguator + | `Field of 'name * 'name constructor ] + [@@deriving show, hash, compare, sexp, hash, eq, map] + (** [poly] is the (polymorphic) type for a relational chunk: it defines what is a chunk. *) + + type t = (DisambiguatedString.t, disambiguator) poly + [@@deriving show, hash, compare, sexp, hash, eq] + (** [t] is the natural instantiation of [poly]. *) + + (** Transforms a [t] into a [poly] with annotated strings instead of just + disambiguators. This adds names to the disambiguator-only constructs defined in + [poly]. *) + let add_strings ?(impl = "impl") ?(anon_const = "anon_const") + ?(foreign = "foregin") ?(global_asm = "global_asm") (n : t) : + (DisambiguatedString.t, DisambiguatedString.t) poly = + let f disambiguator = + DisambiguatedString.{ disambiguator; data = impl } + in + match map_poly Fn.id f n with + | `AnonConst o -> `AnonConst { o with data = anon_const } + | `Foreign o -> `Foreign { o with data = foreign } + | `GlobalAsm o -> `GlobalAsm { o with data = global_asm } + | n -> n + + (** Erases names from a [t]. *) + let only_disambiguators : t -> (disambiguator, disambiguator) poly = + map_poly DisambiguatedString.(fun ds -> ds.disambiguator) Fn.id + + (** Collects all the data of a [t], from the child to the parent. *) + let rec collect_either : + 'n 'd. ('n, 'd) poly -> [ `N of 'n | `D of 'd ] list = function + | `Opaque n + | `GlobalAsm n + | `AnonConst n + | `Impl (n, _, _) + | `Use n + | `Foreign n -> + [ `D n ] + | `Static n + | `Macro n + | `Enum n + | `Struct n + | `Union n + | `TraitAlias n + | `Fn n + | `Const n + | `Trait (n, _) + | `ExternCrate n + | `Mod n + | `ForeignTy n -> + [ `N n ] + | `AssociatedItem ((`Fn a | `Const a | `Type a), b) -> + `N a :: collect_either (b :> _ poly) + | `Constructor (a, b) -> `N a :: collect_either (b :> _ poly) + | `Field (a, b) -> `N a :: collect_either (b :> _ poly) + + (** Same as [collect_either], but works on a [poly] whose ['name] and + ['disambiguator] happen to be the same type. *) + let collect : 'a. ('a, 'a) poly -> 'a list = + fun n -> collect_either n |> List.map ~f:(function `D v | `N v -> v) + + (** Find the root of a [poly]. *) + let root : 'a. ('a, 'a) poly -> 'a = fun x -> collect x |> List.last_exn + end + + type t = Chunk.t list [@@deriving show, hash, compare, sexp, hash, eq] +end + +type t = { mod_path : ModPath.t; rel_path : RelPath.t } +[@@deriving show, hash, compare, sexp, hash, eq] +(** Invariant: [name_path] is non-empty *) diff --git a/engine/lib/concrete_ident/explicit_def_id.ml b/engine/lib/concrete_ident/explicit_def_id.ml new file mode 100644 index 000000000..2bc176b7c --- /dev/null +++ b/engine/lib/concrete_ident/explicit_def_id.ml @@ -0,0 +1,127 @@ +open! Prelude + +module T = struct + type t = { is_constructor : bool; def_id : Types.def_id_contents } + [@@deriving show, yojson, sexp] + + type repr = bool * string * Types.disambiguated_def_path_item list + [@@deriving hash, compare, eq] + + let to_repr { is_constructor; def_id } = + (is_constructor, def_id.krate, def_id.path) + + let hash = to_repr >> hash_repr + let hash_fold_t s = to_repr >> hash_fold_repr s + let equal x y = equal_repr (to_repr x) (to_repr y) + let compare x y = compare_repr (to_repr x) (to_repr y) +end + +include T + +(** Helpers for dealing with Rust raw [Types.def_id]s *) +module H = struct + let contents (did : Types.def_id) = did.contents.value + + (** Helper to get the parent of a [Types.def_id_contents] *) + let parent (did : Types.def_id_contents) : Types.def_id_contents option = + Option.map ~f:contents did.parent +end + +(** A pure, def_id_contents version of [of_def_id]. This is not exposed publicly. *) +let pure_of_def_id ?constructor (def_id : Types.def_id_contents) : t option = + let* _not_crate_root = def_id.path |> List.last in + let path_without_ctor = + (* Get rid of extra [Ctor] *) + let* init, last = last_init def_id.path in + let*? _ = [%matches? Types.Ctor] last.data in + Some init + in + let parent = def_id.parent in + let parent = + if Option.is_some path_without_ctor then + let* parent = parent in + (H.contents parent).parent + else parent + in + let path = Option.value path_without_ctor ~default:def_id.path in + let def_id = { def_id with parent; path } in + let constructor = + if Option.is_some path_without_ctor then Some true else constructor + in + let*? _constructor_provided_if_union_or_struct = + not + (Option.is_none constructor + && [%matches? (Union | Struct : Types.def_kind)] def_id.kind) + in + let is_constructor = + [%matches? (Variant : Types.def_kind)] def_id.kind + || [%matches? Some true] constructor + in + Some { is_constructor; def_id } + +module State = struct + let state = Hash_set.create (module T) + + let of_def_id' ?constructor def_id_contents = + let* did = pure_of_def_id ?constructor def_id_contents in + Hash_set.add state did; + Some did + + let of_def_id ?constructor def_id = + of_def_id' ?constructor (H.contents def_id) + + let list_all () = Hash_set.to_list state +end + +let of_def_id = State.of_def_id + +let of_def_id_exn ?constructor def_id = + of_def_id ?constructor def_id |> Option.value_exn + +let parent (did : t) : t option = + let* parent = H.parent did.def_id in + let*? _not_crate_root = List.is_empty parent.path |> not in + let constructor = [%matches? (Field : Types.def_kind)] did.def_id.kind in + State.of_def_id' ~constructor parent + +let rec parents (did : t) = + did :: (parent did |> Option.map ~f:parents |> Option.value ~default:[]) + +let to_def_id { def_id; _ } = def_id +let is_constructor { is_constructor; _ } = is_constructor + +(** Stateful store that maps [def_id]s to implementation informations +(which trait is implemented? for which type? under which constraints?) *) +module ImplInfoStore = struct + let state : (Types.def_id_contents, Types.impl_infos) Hashtbl.t option ref = + ref None + + module T = struct + type t = Types.def_id_contents [@@deriving show, compare, sexp, eq, hash] + end + + let init (impl_infos : (Types.def_id * Types.impl_infos) list) = + state := + impl_infos + |> List.map ~f:(fun ((id : Types.def_id), impl_infos) -> + (id.contents.value, impl_infos)) + |> Hashtbl.of_alist_multi (module T) + |> Hashtbl.map ~f:List.hd_exn |> Option.some + + let get_state () = + match !state with + | None -> failwith "ImplInfoStore was not initialized" + | Some state -> state + + (** Given a [id] of type [def_id], [find id] will return [Some + impl_info] when [id] is an (non-inherent[1]) impl. [impl_info] + contains information about the trait being implemented and for + which type. + + [1]: https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations + *) + let find k = Hashtbl.find (get_state ()) k + + let lookup_raw (impl_def_id : t) : Types.impl_infos option = + find (to_def_id impl_def_id) +end diff --git a/engine/lib/concrete_ident/explicit_def_id.mli b/engine/lib/concrete_ident/explicit_def_id.mli new file mode 100644 index 000000000..ba67d86d1 --- /dev/null +++ b/engine/lib/concrete_ident/explicit_def_id.mli @@ -0,0 +1,83 @@ +open! Prelude + +(** An [ExplicitDefId.t] is a Rust [Types.def_id] tagged with some diambiguation metadata. + Explicit definition identifiers are used internally by the concrete names of hax. + + Rust raw [Types.def_id] can be ambiguous: consider the following Rust code: + ```rust + struct S; + fn f() -> S { S } + ``` + Here, the return type of `f` (that is, `S`) and the constructor `S` in the body of `f` refers to the exact same identifier `mycrate::S`. + Yet, they denotes two very different objects: a type versus a constructor. + + [ExplicitDefId.t] clears up this ambiguity, making constructors and types two separate things. + + Also, an [ExplicitDefId.t] always points to an item: an [ExplicitDefId.t] is never pointing to a crate alone. +*) + +type t [@@deriving show, yojson, hash, compare, sexp, hash, eq] +(** Representation of explicit definition identifiers. *) + +val of_def_id : ?constructor:bool -> Types.def_id -> t option +(** Smart constructor for [t]. + Creates an explicit def id out of a raw Rust definition identifier [Types.def_id]. + + When [of_def_id] is called with [id] a [Types.def_id], if the [kind] of [id] is either [Struct] or [Union], then [constructor] is mandatory. + Otherwise, the argument [constructor] should be [true] only if [id] is a variant. + + [of_def_id] shall not be called on a Rust identifier pointing to a crate root. + + This function returns [Some] only when those condition are met. + *) + +val of_def_id_exn : ?constructor:bool -> Types.def_id -> t +(** Exception-throwing variant of [make]. + This should be used when we know statically that the conditions + described in the documentation of [make] are met. + + For instance, with static [Types.def_id]s or in [Import_thir]. + *) + +val is_constructor : t -> bool +(** Checks wether a definition identifier [id] points to a constructor. + + [is_constructor id] returns [true] when: + - the kind of [id] is [Struct] or [Union] and the identifier was tagged as a constructor; + - the kind of [id] is [Variant]. + Otherwise, [is_constructor id] returns [false]. + *) + +val parent : t -> t option +(** Looks up the parent of a definition identifier. + Note that the parent of the identifier of a field is always a constructor. + + Also, a top-level item (e.g. `my_crate::some_item`) has no parent: recall that [t] represent only items, not crates. + *) + +val parents : t -> t list +(** Ordered list of parents for an identifier [id], starting with [id], up to the top-most parent identifier. *) + +val to_def_id : t -> Types.def_id_contents +(** Destructor for [t]. *) + +module State : sig + val list_all : unit -> t list + (** List all identifiers the engine dealt with so far. Beware, this function is stateful. *) +end + +module ImplInfoStore : sig + val init : (Types.def_id * Types.impl_infos) list -> unit + + val lookup_raw : t -> Types.impl_infos option + (** Lookup the (raw[1]) implementation informations given a concrete + ident. Returns `Some _` if and only if the supplied identifier points + to an `Impl`. + + [1]: those are raw THIR types. + + {b WARNING}: due to {{: https://github.com/hacspec/hax/issues/363} + issue 363}, when looking up certain identifiers generated by the + engine, this function may return [None] even though the supplied + identifier points to an [Impl] block. *) +end diff --git a/engine/lib/concrete_ident/impl_infos.ml b/engine/lib/concrete_ident/impl_infos.ml index 175d058d1..995cc1a16 100644 --- a/engine/lib/concrete_ident/impl_infos.ml +++ b/engine/lib/concrete_ident/impl_infos.ml @@ -21,7 +21,7 @@ engine, this function may return [None] even though the supplied identifier points to an [Impl] block. *) let lookup span (impl : Concrete_ident.t) : t option = let* Types.{ generics = _; clauses; typ; trait_ref } = - Concrete_ident.lookup_raw_impl_info impl + Concrete_ident.ImplInfoStore.lookup_raw impl in let trait_goal = Option.map ~f:(Import_thir.import_trait_ref span) trait_ref diff --git a/engine/lib/concrete_ident/thir_simple_types.ml b/engine/lib/concrete_ident/thir_simple_types.ml new file mode 100644 index 000000000..55b7fbe28 --- /dev/null +++ b/engine/lib/concrete_ident/thir_simple_types.ml @@ -0,0 +1,78 @@ +open! Prelude +module View = Concrete_ident_view + +(** Interprets a type as a "simple type". + A simple type is a type for which, in a given scope, we can give a non-ambiguous string identifier. + + This is useful for naming local impls. + + Examples of "simple" types: + - primitive types (e.g. u8, u16) + - enums/structs/unions defined in [namespace], when: + + all their generic arguments are instantiated to a simple type + - a reference to a simple type + - a slice to a simple type + - a tuple of simple types of arity zero (e.g. no ADTs of non-zero arity) +*) +let to_string ~(namespace : View.ModPath.t) : + Types.node_for__ty_kind -> string option = + let escape = + let re = Re.Pcre.regexp "_((?:e_)*)of_" in + let f group = "_e_" ^ Re.Group.get group 1 ^ "of_" in + Re.replace ~all:true re ~f + in + let adt def_id = + let* def_id = Explicit_def_id.of_def_id ~constructor:false def_id in + let view = View.of_def_id def_id in + let* () = + [%equal: View.ModPath.t] view.mod_path namespace |> some_if_true + in + let* last = expect_singleton view.rel_path in + let* name = + match last with + | (`Struct d | `Union d | `Enum d) + when Int64.(equal (of_int 0) d.disambiguator) -> + Some d.data + | _ -> None + in + escape name |> Option.some + in + let arity0 (ty : Types.node_for__ty_kind) = + match ty.Types.value with + | Bool -> Some "bool" + | Char -> Some "char" + | Str -> Some "str" + | Never -> Some "never" + | Int Isize -> Some "isize" + | Int I8 -> Some "i8" + | Int I16 -> Some "i16" + | Int I32 -> Some "i32" + | Int I64 -> Some "i64" + | Int I128 -> Some "i128" + | Uint Usize -> Some "usize" + | Uint U8 -> Some "u8" + | Uint U16 -> Some "u16" + | Uint U32 -> Some "u32" + | Uint U64 -> Some "u64" + | Uint U128 -> Some "u128" + | Float F32 -> Some "f32" + | Float F64 -> Some "f64" + | Tuple [] -> Some "unit" + | Adt { def_id; generic_args = []; _ } -> Option.map ~f:escape (adt def_id) + | _ -> None + in + let apply left right = left ^ "_of_" ^ right in + let rec arity1 (ty : Types.node_for__ty_kind) = + match ty.value with + | Slice sub -> arity1 sub |> Option.map ~f:(apply "slice") + | Ref (_, sub, _) -> arity1 sub |> Option.map ~f:(apply "ref") + | Adt { def_id; generic_args = [ Type arg ]; _ } -> + let* adt = adt def_id in + let* arg = arity1 arg in + Some (apply adt arg) + | Tuple l -> + let* l = List.map ~f:arity0 l |> Option.all in + Some ("tuple_" ^ String.concat ~sep:"_" l) + | _ -> arity0 ty + in + arity1 diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index 19e5ff1ad..dc7034c11 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -6,25 +6,45 @@ module Make (F : Features.T) = struct open Ast open AST - let ident_of (item : item) : Concrete_ident.t = - match item.v with Type { name; _ } -> name | _ -> item.ident + (** Get the identifier of an item *) + let ident_of (item : item) : Concrete_ident.t = item.ident + + (** Get all the identifiers declared under an item. This includes the + identifier of the item itself, but also of any sub-item: for instance, + associated items within an impl. *) + let idents_of (item : item) : Concrete_ident.t list = + let is_field_anonymous ident = + match List.last (Concrete_ident.to_view ident).mod_path with + | Some { data = n; _ } -> Option.is_some (Int.of_string_opt n) + | _ -> false + in + ident_of item + :: + (match item.v with + | Type { variants; _ } -> + List.concat_map + ~f:(fun variant -> + let fields = + List.map ~f:fst3 variant.arguments + |> List.filter ~f:is_field_anonymous + in + + variant.name :: fields) + variants + | Trait { items; _ } -> List.map ~f:(fun item -> item.ti_ident) items + | Impl { items; _ } -> List.map ~f:(fun item -> item.ii_ident) items + | _ -> (* No sub items *) []) module Namespace = struct - module T = struct - type t = string list [@@deriving show, yojson, compare, sexp, eq, hash] - end - - module TT = struct - include T - include Comparator.Make (T) - end + include Concrete_ident.View.ModPath + module Set = Set.M (Concrete_ident.View.ModPath) - include TT - module Set = Set.M (TT) + let of_concrete_ident ci : t = (Concrete_ident.to_view ci).mod_path - let of_concrete_ident ci : t = - let krate, path = Concrete_ident.DefaultViewAPI.to_namespace ci in - krate :: path + let to_string ?(sep = "::") : t -> string = + List.map ~f:(fun (o : Concrete_ident_view.DisambiguatedString.t) -> + o.data) + >> String.concat ~sep end module Error : Phase_utils.ERROR = Phase_utils.MakeError (struct @@ -172,13 +192,12 @@ module Make (F : Features.T) = struct (mod_graph_cycles : Namespace.Set.t list) : Bundle.t list = let item_names = List.map items ~f:(fun x -> x.ident) in let cycles = - List.filter mod_graph_cycles ~f:(fun set -> - Prelude.Set.length set > 1) + List.filter mod_graph_cycles ~f:(fun set -> Set.length set > 1) in let bundles = List.map cycles ~f:(fun set -> List.filter item_names ~f:(fun item -> - Prelude.Set.mem set (Namespace.of_concrete_ident item))) + Set.mem set (Namespace.of_concrete_ident item))) in bundles end @@ -191,12 +210,12 @@ module Make (F : Features.T) = struct let vertex_name i = "\"" ^ Concrete_ident.show i ^ "\"" let vertex_attributes i = - [ `Label (Concrete_ident.DefaultViewAPI.to_definition_name i) ] + [ `Label (Concrete_ident.DefaultViewAPI.render i).name ] let get_subgraph i = let ns = Namespace.of_concrete_ident i in - let sg_name = String.concat ~sep:"__" ns in - let label = String.concat ~sep:"::" ns in + let sg_name = Namespace.to_string ~sep:"__" ns in + let label = Namespace.to_string ~sep:"::" ns in let open Graph.Graphviz.DotAttributes in Some { sg_name; sg_attributes = [ `Label label ]; sg_parent = None } @@ -236,7 +255,7 @@ module Make (F : Features.T) = struct let graph_attributes _ = [] let default_vertex_attributes _ = [] - let vertex_name ns = "\"" ^ String.concat ~sep:"::" ns ^ "\"" + let vertex_name ns = "\"" ^ Namespace.to_string ns ^ "\"" let vertex_attributes _ = [] let get_subgraph _ = None let default_edge_attributes _ = [] @@ -372,106 +391,41 @@ module Make (F : Features.T) = struct in List.filter ~f:(ident_of >> Set.mem selection) items - (* Construct the new item `f item` (say `item'`), and create a - "symbolic link" to `item'`. Returns a pair that consists in the - symbolic link and in `item'`. *) - let shallow_copy (f : item -> item) - (variants_renamings : - concrete_ident * concrete_ident -> - (concrete_ident * concrete_ident) list) (item : item) : item list = - let item' = f item in - let old_new = (ident_of item, ident_of item') in + let fresh_module_for (bundle : item list) = + let fresh_module = + Concrete_ident.fresh_module ~label:"bundle" (List.map ~f:ident_of bundle) + in + let renamings = + bundle + (* Exclude `Use` items: we exclude those from bundling since they are only + user hints. `Use` items don't have proper identifiers, and those + identifiers are never referenced by other Rust items. *) + |> List.filter ~f:(function { v = Use _; _ } -> false | _ -> true) + (* Exclude `NotImplementedYet` items *) + |> List.filter ~f:(function + | { v = NotImplementedYet; _ } -> false + | _ -> true) + |> List.concat_map ~f:(fun item -> + List.map + ~f:(fun id -> + ( item, + (id, Concrete_ident.move_to_fresh_module fresh_module id) )) + (idents_of item)) + in let aliases = - List.map (old_new :: variants_renamings old_new) - ~f:(fun (old_ident, new_ident) -> + List.map renamings ~f:(fun (origin_item, (from_id, to_id)) -> let attrs = - List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs + List.filter + ~f:(fun att -> Attrs.late_skip [ att ]) + origin_item.attrs in - - { item with v = Alias { name = old_ident; item = new_ident }; attrs }) - in - item' :: aliases - - let bundle_cyclic_modules (items : item list) : item list = - let from_ident ident : item option = - List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items + let v = Alias { name = from_id; item = to_id } in + { attrs; span = origin_item.span; ident = from_id; v }) in - let mut_rec_bundles = - let mod_graph_cycles = ModGraph.of_items items |> ModGraph.cycles in - (* `Use` items shouldn't be bundled as they have no dependencies - and they have dummy names. *) - let non_use_items = - List.filter - ~f:(fun item -> - match item.v with Use _ | NotImplementedYet -> false | _ -> true) - items - in - let bundles = - ItemGraph.CyclicDep.of_mod_sccs non_use_items mod_graph_cycles - in - let f = List.filter_map ~f:from_ident in - List.map ~f bundles - in - - let transform (bundle : item list) = - let module_names = - List.map ~f:(ident_of >> Concrete_ident.Create.parent) bundle - |> List.dedup_and_sort ~compare:Concrete_ident.compare - in - let ns : Concrete_ident.t = - Concrete_ident.Create.fresh_module ~from:module_names - in - let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t = - Concrete_ident.Create.move_under ~new_parent:ns - in - let new_names = List.map ~f:(ident_of >> new_name_under_ns) bundle in - let duplicates = - new_names |> List.find_all_dups ~compare:Concrete_ident.compare - in - (* Verify name clashes *) - (* In case of clash, add hash *) - let add_prefix id = - if - not - (List.mem duplicates (new_name_under_ns id) - ~equal:Concrete_ident.equal) - then id - else Concrete_ident.Create.add_disambiguator id (Concrete_ident.hash id) - in + let rename = + let renamings = List.map ~f:snd renamings in let renamings = - List.map - ~f:(ident_of >> (Fn.id &&& (add_prefix >> new_name_under_ns))) - bundle - in - let variants_renamings (previous_name, new_name) = - match from_ident previous_name with - | Some { v = Type { variants; is_struct = false; _ }; _ } -> - List.map variants ~f:(fun { name; _ } -> - ( name, - Concrete_ident.Create.move_under ~new_parent:new_name name )) - | Some { v = Type { variants; is_struct = true; _ }; _ } -> - List.concat_map variants ~f:(fun { arguments; _ } -> - List.map arguments ~f:(fun (name, _, _) -> - ( name, - Concrete_ident.Create.move_under ~new_parent:new_name name - ))) - | _ -> [] - in - let variant_and_constructors_renamings = - List.concat_map ~f:variants_renamings renamings - |> List.concat_map ~f:(fun (old_name, new_name) -> - [ - (old_name, new_name); - ( Concrete_ident.Create.constructor old_name, - Concrete_ident.Create.constructor new_name ); - ]) - in - let renamings = - match - Map.of_alist - (module Concrete_ident) - (renamings @ variant_and_constructors_renamings) - with + match Map.of_alist (module Concrete_ident) renamings with | `Duplicate_key dup -> failwith [%string @@ -481,47 +435,25 @@ module Make (F : Features.T) = struct %{[%show: concrete_ident] dup}"] | `Ok value -> value in - let rename = - let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in - (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel - in - fun it -> shallow_copy rename variants_renamings it - in - let bundle_transforms = - List.concat_map mut_rec_bundles ~f:(fun bundle -> - let bundle_value = - ( List.map ~f:ident_of bundle - |> ItemGraph.MutRec.Bundle.homogeneous_namespace, - transform bundle ) - in - List.map bundle ~f:(fun item -> (item, bundle_value))) + let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in + (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel in - let module ComparableItem = struct - module T = struct - type t = item [@@deriving sexp_of, compare, hash] - end + List.map ~f:rename bundle @ aliases - include T - include Comparable.Make (T) - end in - let bundle_of_item = - match Hashtbl.of_alist (module ComparableItem) bundle_transforms with - | `Duplicate_key dup -> - failwith - [%string - "Fatal error: in dependency analysis, [bundles_transforms] is \ - expected to be a key-value list with a guarantee of unicity in \ - keys. However, we found the following key (an item) twice:\n\ - %{U.Debug.item' dup}"] - | `Ok value -> value - in - let maybe_transform_item item = - match Hashtbl.find bundle_of_item item with - | Some (homogeneous_bundle, transform_bundle) -> - if homogeneous_bundle then [ item ] else transform_bundle item - | None -> [ item ] + let bundle_cyclic_modules (items : item list) : item list = + (* [module_level_scc] is a list of set of strongly connected modules. *) + let module_level_scc = ModGraph.(of_items >> cycles) items in + let items_per_ns = + List.map ~f:(fun i -> (Namespace.of_concrete_ident i.ident, i)) items + |> Map.of_alist_multi (module Namespace) in - List.concat_map items ~f:maybe_transform_item + let items_of_ns = Map.find items_per_ns >> Option.value ~default:[] in + module_level_scc + |> List.concat_map ~f:(fun nss -> + let multiple_heterogeneous_modules = Set.length nss > 1 in + let items = Set.to_list nss |> List.concat_map ~f:items_of_ns in + if multiple_heterogeneous_modules then fresh_module_for items + else items) let recursive_bundles (items : item list) : item list list * item list = let g = ItemGraph.of_items ~original_items:items items in diff --git a/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml b/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml index 37fe9bc4c..4b52400d7 100644 --- a/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml +++ b/engine/lib/deprecated_generic_printer/deprecated_generic_printer.ml @@ -1,7 +1,7 @@ open! Prelude open! Ast -module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct +module Make (F : Features.T) (View : Concrete_ident.RENDER_API) = struct open Deprecated_generic_printer_base open Deprecated_generic_printer_base.Make (F) @@ -31,19 +31,20 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct method namespace_of_concrete_ident : concrete_ident -> string * string list = - fun i -> View.to_namespace i + fun i -> + let rendered = View.render i in + (rendered.name, rendered.path) method concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = fun id -> - let id = View.to_view id in + let id = View.render id in let chunks = - if under_current_ns then [ id.definition ] - else id.crate :: (id.path @ [ id.definition ]) + if under_current_ns then [ id.name ] else id.path @ [ id.name ] in separate_map (colon ^^ colon) utf8string chunks method name_of_concrete_ident : concrete_ident fn = - View.to_definition_name >> utf8string + fun id -> (View.render id).name |> utf8string method mutability : 'a. 'a mutability fn = fun _ -> empty diff --git a/engine/lib/deprecated_generic_printer/deprecated_generic_printer.mli b/engine/lib/deprecated_generic_printer/deprecated_generic_printer.mli index 3eb3904f6..fdf32ccba 100644 --- a/engine/lib/deprecated_generic_printer/deprecated_generic_printer.mli +++ b/engine/lib/deprecated_generic_printer/deprecated_generic_printer.mli @@ -1,4 +1,4 @@ -module Make (F : Features.T) (View : Concrete_ident.VIEW_API) : sig +module Make (F : Features.T) (View : Concrete_ident.RENDER_API) : sig open Deprecated_generic_printer_base.Make(F) include API diff --git a/engine/lib/dune b/engine/lib/dune index 17a3db14d..cf6396636 100644 --- a/engine/lib/dune +++ b/engine/lib/dune @@ -1,6 +1,19 @@ (library (public_name hax-engine) (name hax_engine) + ; (modules + ; types + ; concrete_ident + ; concrete_ident_view + ; concrete_ident_defid + ; prelude + ; concrete_ident_view_types + ; concrete_ident_generated + ; concrete_ident_render_sig + ; local_ident + ; thir_simple_types + ; concrete_ident_fresh_ns + ; utils) (libraries yojson non_empty_list @@ -32,6 +45,7 @@ ppx_generate_features ppx_functor_application ppx_enumerate + ppx_deriving.map ppx_matches))) (include_subdirs unqualified) diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml index 81a5c793f..cd8370205 100644 --- a/engine/lib/generic_printer/generic_printer.ml +++ b/engine/lib/generic_printer/generic_printer.ml @@ -171,7 +171,7 @@ module Make (F : Features.T) = struct object (self) inherit Gen.base as super inherit span_helper - val mutable current_namespace : (string * string list) option = None + val mutable current_namespace : string list option = None method private catch_exn (handle : string -> document) (f : unit -> document) : document = @@ -192,7 +192,7 @@ module Make (F : Features.T) = struct method virtual printer_name : string (** Mark a path as unreachable *) - val concrete_ident_view : (module Concrete_ident.VIEW_API) = + val concrete_ident_view : (module Concrete_ident.RENDER_API) = (module Concrete_ident.DefaultViewAPI) (** The concrete ident view to be used *) @@ -221,12 +221,13 @@ module Make (F : Features.T) = struct |> string (** {2:specialize-expr Printers for special types} *) - method concrete_ident ~local (id : Concrete_ident.view) : document = + method concrete_ident ~local (id : Concrete_ident_render_sig.rendered) + : document = string - (if local then id.definition + (if local then id.name else String.concat ~sep:self#module_path_separator - (id.crate :: (id.path @ [ id.definition ]))) + (id.path @ [ id.name ])) (** [concrete_ident ~local id] prints a name without path if [local] is true, otherwise it prints the full path, separated by `module_path_separator`. *) @@ -601,13 +602,9 @@ module Make (F : Features.T) = struct lazy_doc (fun (id : concrete_ident) -> let module View = (val concrete_ident_view) in - let id = View.to_view id in - let ns_crate, ns_path = - Option.value ~default:("", []) current_namespace - in - let local = - String.(ns_crate = id.crate) && [%eq: string list] ns_path id.path - in + let id = View.render id in + let ns_path = Option.value ~default:[] current_namespace in + let local = [%eq: string list] ns_path id.path in self#concrete_ident ~local id) ast_position id @@ -630,7 +627,7 @@ module Make (F : Features.T) = struct method! _do_not_override_lazy_of_item ast_position (value : item) : item lazy_doc = let module View = (val concrete_ident_view) in - current_namespace <- View.to_namespace value.ident |> Option.some; + current_namespace <- Some (View.render value.ident).path; super#_do_not_override_lazy_of_item ast_position value method _do_not_override_lazy_of_generics ast_position (value : generics) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 2b265117a..2a087feb2 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -39,8 +39,8 @@ module U = Ast_utils.Make (Features.Rust) module W = Features.On open Ast -let def_id kind (def_id : Thir.def_id) : global_ident = - `Concrete (Concrete_ident.of_def_id kind def_id) +let def_id ~value (def_id : Thir.def_id) : global_ident = + `Concrete (Concrete_ident.of_def_id ~value def_id) let local_ident kind (ident : Thir.local_ident) : local_ident = { @@ -220,8 +220,7 @@ let resugar_index_mut (e : expr) : (expr * expr) option = | _ -> None (** Name for the cast function from an ADT to its discriminant *) -let cast_name_for_type typ_name = - Concrete_ident.Create.map_last ~f:(fun s -> s ^ "_cast_to_repr") typ_name +let cast_name_for_type = Concrete_ident.with_suffix `Cast module type EXPR = sig val c_expr : Thir.decorated_for__expr_kind -> expr @@ -343,15 +342,15 @@ end) : EXPR = struct in match f (lhs.typ, rhs.typ) with | Some with_ -> - Concrete_ident.of_name Value name - |> Concrete_ident.map_path_strings ~f:(function + Concrete_ident.of_name ~value:true name + |> (Concrete_ident.map_path_strings [@alert "-unsafe"]) ~f:(function | "u128" -> with_ | s -> s) | None -> assertion_failure (Span.to_thir span) ("Binary operation: expected " ^ expected ^ " type, got " ^ [%show: ty] lhs.typ) - else Concrete_ident.of_name Value @@ overloaded_names_of_binop op + else Concrete_ident.of_name ~value:true @@ overloaded_names_of_binop op in U.call' (`Concrete name) [ lhs; rhs ] span typ @@ -372,7 +371,9 @@ end) : EXPR = struct and c_expr_drop_body (e : Thir.decorated_for__expr_kind) : expr = let typ = c_ty e.span e.ty in let span = Span.of_thir e.span in - let v = Global_ident.of_name Value Rust_primitives__hax__dropped_body in + let v = + Global_ident.of_name ~value:true Rust_primitives__hax__dropped_body + in { span; typ; e = GlobalVar v } and c_block ~expr ~span ~stmts ~ty ~(safety_mode : Types.block_safety) : expr @@ -472,7 +473,7 @@ end) : EXPR = struct MacroInvokation { args = argument; - macro = def_id Macro macro_ident; + macro = def_id ~value:false macro_ident; witness = W.macro; } | If @@ -519,7 +520,7 @@ end) : EXPR = struct let f = c_expr fun' in match (trait, fun'.contents) with | Some _, GlobalName { id; _ } -> - { f with e = GlobalVar (def_id (AssociatedItem Value) id) } + { f with e = GlobalVar (def_id ~value:true id) } | _ -> f in let args = if List.is_empty args then [ unit_expr span ] else args in @@ -610,7 +611,8 @@ end) : EXPR = struct let lhs = c_expr lhs in let projector = GlobalVar - (`Projector (`Concrete (Concrete_ident.of_def_id Field field))) + (`Projector + (`Concrete (Concrete_ident.of_def_id ~value:true field))) in let span = Span.of_thir e.span in App @@ -638,15 +640,7 @@ end) : EXPR = struct trait = None (* TODO: see issue #328 *); bounds_impls = []; } - | GlobalName { id; constructor } -> - let kind = - match constructor with - | Some { kind = Struct _; _ } -> - Concrete_ident.Kind.Constructor { is_struct = true } - | Some _ -> Concrete_ident.Kind.Constructor { is_struct = false } - | None -> Concrete_ident.Kind.Value - in - GlobalVar (def_id kind id) + | GlobalName { id; constructor = _ } -> GlobalVar (def_id ~value:true id) | UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident Expr id) | Borrow { arg; borrow_kind = kind } -> let e' = c_expr arg in @@ -702,7 +696,7 @@ end) : EXPR = struct unimplemented ~issue_id:998 [ e.span ] "Construct union types: not supported" in - let constructor = def_id (Constructor { is_struct }) info.variant in + let constructor = def_id ~value:true info.variant in let base = Option.map ~f:(fun base -> (c_expr base.base, W.construct_base)) @@ -711,7 +705,7 @@ end) : EXPR = struct let fields = List.map ~f:(fun f -> - let field = def_id Field f.field in + let field = def_id ~value:true f.field in let value = c_expr f.value in (field, value)) fields @@ -731,10 +725,7 @@ end) : EXPR = struct }) l)) | NamedConst { def_id = id; impl; args; _ } -> ( - let kind : Concrete_ident.Kind.t = - match impl with Some _ -> AssociatedItem Value | _ -> Value - in - let f = GlobalVar (def_id kind id) in + let f = GlobalVar (def_id ~value:true id) in match impl with | Some impl -> let trait = @@ -762,9 +753,9 @@ end) : EXPR = struct let lhs_type = c_ty lhs.span lhs.ty in call (mk_global ([ lhs_type; index_type ] ->. typ) - @@ Global_ident.of_name Value Core__ops__index__Index__index) + @@ Global_ident.of_name ~value:true Core__ops__index__Index__index) [ lhs; index ] - | StaticRef { def_id = id; _ } -> GlobalVar (def_id Value id) + | StaticRef { def_id = id; _ } -> GlobalVar (def_id ~value:true id) | PlaceTypeAscription _ -> assertion_failure [ e.span ] "Got a unexpected node `PlaceTypeAscription`. Please report, we \ @@ -900,7 +891,7 @@ end) : EXPR = struct unimplemented ~issue_id:998 [ pat.span ] "Pattern match on union types: not supported" in - let constructor = def_id (Constructor { is_struct }) info.variant in + let constructor = def_id ~value:true info.variant in let fields = List.map ~f:(c_field_pat info) subpatterns in PConstruct { constructor; fields; is_record; is_struct } | Tuple { subpatterns } -> @@ -937,7 +928,10 @@ end) : EXPR = struct { p = v; span; typ } and c_field_pat _info (field_pat : Thir.field_pat) : field_pat = - { field = def_id Field field_pat.field; pat = c_pat field_pat.pattern } + { + field = def_id ~value:true field_pat.field; + pat = c_pat field_pat.pattern; + } and extended_literal_of_expr (e : expr) : extended_literal = let not_a_literal () = @@ -1016,7 +1010,7 @@ end) : EXPR = struct in TArrow (inputs, c_ty span output) | Adt { def_id = id; generic_args; _ } -> - let ident = def_id Type id in + let ident = def_id ~value:false id in let args = List.map ~f:(c_generic_value span) generic_args in TApp { ident; args } | Foreign _ -> unimplemented ~issue_id:928 [ span ] "Foreign" @@ -1037,10 +1031,10 @@ end) : EXPR = struct TApp { ident = `TupleType (List.length types); args = types } | Alias { kind = Projection { assoc_item = _; impl_expr }; def_id; _ } -> let impl = c_impl_expr span impl_expr in - let item = Concrete_ident.of_def_id (AssociatedItem Type) def_id in + let item = Concrete_ident.of_def_id ~value:false def_id in TAssociatedType { impl; item } | Alias { kind = Opaque _; def_id; _ } -> - TOpaque (Concrete_ident.of_def_id Type def_id) + TOpaque (Concrete_ident.of_def_id ~value:false def_id) | Alias { kind = Inherent; _ } -> assertion_failure [ span ] "Ty::Alias with AliasTyKind::Inherent" | Alias { kind = Weak; _ } -> @@ -1068,7 +1062,7 @@ end) : EXPR = struct | Trait { args; def_id } -> let goal : dyn_trait_goal = { - trait = Concrete_ident.of_def_id Trait def_id; + trait = Concrete_ident.of_def_id ~value:false def_id; non_self_args = List.map ~f:(c_generic_value span) args; } in @@ -1106,7 +1100,7 @@ end) : EXPR = struct { kind = ImplApp { impl; args }; goal } and c_trait_ref span (tr : Thir.trait_ref) : trait_goal = - let trait = Concrete_ident.of_def_id Trait tr.def_id in + let trait = Concrete_ident.of_def_id ~value:false tr.def_id in let args = List.map ~f:(c_generic_value span) tr.generic_args in { trait; args } @@ -1121,10 +1115,7 @@ end) : EXPR = struct let ident = { goal = c_trait_ref span trait_ref; name = predicate_id } in - let kind : Concrete_ident.Kind.t = - match item.kind with Const | Fn -> Value | Type -> Type - in - let item = Concrete_ident.of_def_id kind item.def_id in + let item = Concrete_ident.of_def_id ~value:false item.def_id in let trait_ref = c_trait_ref span trait_ref in Projection { impl = { kind = item_kind; goal = trait_ref }; ident; item } @@ -1138,7 +1129,7 @@ end) : EXPR = struct in match ie with | Concrete { id; generics } -> - let trait = Concrete_ident.of_def_id Impl id in + let trait = Concrete_ident.of_def_id ~value:false id in let args = List.map ~f:(c_generic_value span) generics in Concrete { trait; args } | LocalBound { predicate_id; path; _ } -> @@ -1234,12 +1225,12 @@ end) : EXPR = struct match kind with | Trait { is_positive = true; trait_ref } -> let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in - let trait = Concrete_ident.of_def_id Trait trait_ref.def_id in + let trait = Concrete_ident.of_def_id ~value:false trait_ref.def_id in Some (GCType { goal = { trait; args }; name = id }) | Projection { impl_expr; assoc_item; ty } -> let impl = c_impl_expr span impl_expr in let assoc_item = - Concrete_ident.of_def_id (AssociatedItem Type) assoc_item.def_id + Concrete_ident.of_def_id ~value:false assoc_item.def_id in let typ = c_ty span ty in Some (GCProjection { impl; assoc_item; typ }) @@ -1335,7 +1326,7 @@ let c_trait_item (item : Thir.trait_item) : trait_item = let open (val make ~krate:item.owner_id.contents.value.krate : EXPR) in let { params; constraints } = c_generics item.generics in (* TODO: see TODO in impl items *) - let ti_ident = Concrete_ident.of_def_id Field item.owner_id in + let ti_ident = Concrete_ident.of_def_id ~value:false item.owner_id in { ti_span = Span.of_thir item.span; ti_generics = { params; constraints }; @@ -1418,7 +1409,9 @@ let cast_of_enum typ_name generics typ thir_span let acc = Lit Int64.(n + m) in (acc, (pat, acc)) | _, Explicit did -> - let acc = Exp { e = GlobalVar (def_id Value did); span; typ } in + let acc = + Exp { e = GlobalVar (def_id ~value:true did); span; typ } + in (acc, (pat, acc)) | Exp e, Relative n -> let acc = @@ -1524,7 +1517,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = mk @@ Fn { - name = Concrete_ident.of_def_id Value (assert_item_def_id ()); + name = Concrete_ident.of_def_id ~value:true (assert_item_def_id ()); generics = c_generics generics; body = c_body body; params = []; @@ -1534,7 +1527,8 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = mk @@ TyAlias { - name = Concrete_ident.of_def_id Type (assert_item_def_id ()); + name = + Concrete_ident.of_def_id ~value:false (assert_item_def_id ()); generics = c_generics generics; ty = c_ty item.span ty; } @@ -1542,7 +1536,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = mk @@ Fn { - name = Concrete_ident.of_def_id Value (assert_item_def_id ()); + name = Concrete_ident.of_def_id ~value:true (assert_item_def_id ()); generics = c_generics generics; body = c_body body; params = c_fn_params item.span params; @@ -1552,18 +1546,17 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let generics = c_generics generics in let is_struct = match item.kind with Struct _ -> true | _ -> false in let def_id = assert_item_def_id () in - let name = Concrete_ident.of_def_id Type def_id in + let name = Concrete_ident.of_def_id ~value:false def_id in mk @@ Type { name; generics; variants = []; is_struct } | Enum (variants, generics, repr) -> let def_id = assert_item_def_id () in let generics = c_generics generics in let is_struct = false in - let kind = Concrete_ident.Kind.Constructor { is_struct } in let discs = (* Each variant might introduce a anonymous constant defining its discriminant integer *) List.filter_map ~f:(fun v -> v.disr_expr) variants |> List.map ~f:(fun Types.{ def_id; body; _ } -> - let name = Concrete_ident.of_def_id kind def_id in + let name = Concrete_ident.of_def_id ~value:true def_id in let generics = { params = []; constraints = [] } in let body = c_expr body in { @@ -1588,13 +1581,13 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = [%matches? (Struct { fields = _ :: _; _ } : Types.variant_data)] data in - let name = Concrete_ident.of_def_id kind variant_id in + let name = Concrete_ident.of_def_id ~value:true variant_id in let arguments = match data with | Tuple (fields, _, _) | Struct { fields; _ } -> List.map ~f:(fun { def_id = id; ty; span; attributes; _ } -> - ( Concrete_ident.of_def_id Field id, + ( Concrete_ident.of_def_id ~value:true id, c_ty span ty, c_attrs attributes )) fields @@ -1604,7 +1597,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = ({ name; arguments; is_record; attrs }, original)) variants in - let name = Concrete_ident.of_def_id Type def_id in + let name = Concrete_ident.of_def_id ~value:true def_id in let cast_fun = cast_of_enum name generics (c_ty item.span repr.typ) item.span variants in @@ -1619,14 +1612,13 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let is_struct = true in (* repeating the attributes of the item in the variant: TODO is that ok? *) let v = - let kind = Concrete_ident.Kind.Constructor { is_struct } in - let name = Concrete_ident.of_def_id kind def_id in - let name = Concrete_ident.Create.move_under name ~new_parent:name in + let name = Concrete_ident.of_def_id ~value:true def_id in + (* let name = Concrete_ident.Create.move_under name ~new_parent:name in *) let mk fields is_record = let arguments = List.map ~f:(fun Thir.{ def_id = id; ty; span; attributes; _ } -> - ( Concrete_ident.of_def_id Field id, + ( Concrete_ident.of_def_id ~value:true id, c_ty span ty, c_attrs attributes )) fields @@ -1639,13 +1631,13 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = | _ -> { name; arguments = []; is_record = false; attrs } in let variants = [ v ] in - let name = Concrete_ident.of_def_id Type def_id in + let name = Concrete_ident.of_def_id ~value:false def_id in mk @@ Type { name; generics; variants; is_struct } | MacroInvokation { macro_ident; argument; span } -> mk @@ IMacroInvokation { - macro = Concrete_ident.of_def_id Macro macro_ident; + macro = Concrete_ident.of_def_id ~value:false macro_ident; argument; span = Span.of_thir span; witness = W.macro; @@ -1656,7 +1648,9 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = ~f:(fun { attributes; _ } -> not (should_skip attributes)) items in - let name = Concrete_ident.of_def_id Trait (assert_item_def_id ()) in + let name = + Concrete_ident.of_def_id ~value:false (assert_item_def_id ()) + in let { params; constraints } = c_generics generics in let self = let id = Local_ident.mk_id Typ 0 (* todo *) in @@ -1678,7 +1672,9 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = in List.map ~f:(fun (item : Thir.impl_item) -> - let item_def_id = Concrete_ident.of_def_id Impl item.owner_id in + let item_def_id = + Concrete_ident.of_def_id ~value:false item.owner_id + in let attrs = c_item_attrs item.attributes in let sub_item_erased_by_user = erased_by_user attrs in let erased_by_type_only = @@ -1725,7 +1721,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = associated types \ (https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations)." in - let ident = Concrete_ident.of_def_id Value item.owner_id in + let ident = Concrete_ident.of_def_id ~value:false item.owner_id in { span = Span.of_thir item.span; v; ident; attrs }) items | Impl @@ -1757,7 +1753,8 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = params = [ U.make_unit_param span ]; }; ii_ident = - Concrete_ident.of_name Value Rust_primitives__hax__dropped_body; + Concrete_ident.of_name ~value:false + Rust_primitives__hax__dropped_body; ii_attrs = []; }; ] @@ -1768,7 +1765,9 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = something. Otherwise we have to assume every backend will see traits and impls as records. See https://github.com/hacspec/hax/issues/271. *) - let ii_ident = Concrete_ident.of_def_id Field item.owner_id in + let ii_ident = + Concrete_ident.of_def_id ~value:false item.owner_id + in { ii_span = Span.of_thir item.span; ii_generics = c_generics item.generics; @@ -1806,7 +1805,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = generics = c_generics generics; self_ty = c_ty item.span self_ty; of_trait = - ( Concrete_ident.of_def_id Trait of_trait.def_id, + ( Concrete_ident.of_def_id ~value:false of_trait.def_id, List.map ~f:(c_generic_value item.span) of_trait.generic_args ); items; @@ -1835,21 +1834,23 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = (* ident is supposed to always be an actual item, thus here we need to cheat a bit *) (* TODO: is this DUMMY thing really needed? there's a `Use` segment (see #272) *) let def_id = item.owner_id in - let def_id : Types.def_id = - let value = - { - def_id.contents.value with - path = - def_id.contents.value.path - @ [ - Types. - { data = ValueNs "DUMMY"; disambiguator = MyInt64.of_int 0 }; - ]; - } - in - { contents = { def_id.contents with value } } - in - [ { span; v; ident = Concrete_ident.of_def_id Value def_id; attrs } ] + (* let def_id : Types.def_id = + let value = + { + def_id.contents.value with + path = + def_id.contents.value.path + @ [ + Types. + { data = ValueNs "DUMMY"; disambiguator = MyInt64.of_int 0 }; + ]; + } + in + { contents = { def_id.contents with value } } + in *) + [ + { span; v; ident = Concrete_ident.of_def_id ~value:false def_id; attrs }; + ] | Union _ -> unimplemented ~issue_id:998 [ item.span ] "Union types: not supported" | ExternCrate _ | Static _ | Macro _ | Mod _ | ForeignMod _ | GlobalAsm _ @@ -1858,7 +1859,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let import_item ~type_only (item : Thir.item) : concrete_ident * (item list * Diagnostics.t list) = - let ident = Concrete_ident.of_def_id Value item.owner_id in + let ident = Concrete_ident.of_def_id ~value:false item.owner_id in let r, reports = let f = U.Mappers.rename_generic_constraints#visit_item diff --git a/engine/lib/phases/phase_cf_into_monads.ml b/engine/lib/phases/phase_cf_into_monads.ml index d5565c4fb..8683dbd1c 100644 --- a/engine/lib/phases/phase_cf_into_monads.ml +++ b/engine/lib/phases/phase_cf_into_monads.ml @@ -52,16 +52,21 @@ struct | None -> x.typ | Some (MResult err) -> let args = List.map ~f:(fun t -> B.GType t) [ x.typ; err ] in - let ident = Global_ident.of_name Type Core__result__Result in + let ident = + Global_ident.of_name ~value:false Core__result__Result + in TApp { ident; args } | Some MOption -> let args = List.map ~f:(fun t -> B.GType t) [ x.typ ] in - let ident = Global_ident.of_name Type Core__option__Option in + let ident = + Global_ident.of_name ~value:false Core__option__Option + in TApp { ident; args } | Some (MException return) -> let args = List.map ~f:(fun t -> B.GType t) [ return; x.typ ] in let ident = - Global_ident.of_name Type Core__ops__control_flow__ControlFlow + Global_ident.of_name ~value:false + Core__ops__control_flow__ControlFlow in TApp { ident; args } diff --git a/engine/lib/phases/phase_direct_and_mut.ml b/engine/lib/phases/phase_direct_and_mut.ml index c0b557834..bcff1fa29 100644 --- a/engine/lib/phases/phase_direct_and_mut.ml +++ b/engine/lib/phases/phase_direct_and_mut.ml @@ -68,7 +68,8 @@ struct if hax_core_extraction then TApp { - ident = Global_ident.of_name Type Rust_primitives__hax__MutRef; + ident = + Global_ident.of_name ~value:false Rust_primitives__hax__MutRef; args = [ GType (dty span typ) ]; } else Error.raise { kind = UnallowedMutRef; span } diff --git a/engine/lib/phases/phase_drop_match_guards.ml b/engine/lib/phases/phase_drop_match_guards.ml index f54e61a53..14970879a 100644 --- a/engine/lib/phases/phase_drop_match_guards.ml +++ b/engine/lib/phases/phase_drop_match_guards.ml @@ -106,7 +106,7 @@ module%inlined_contents Make (F : Features.T) = struct let opt_result_typ : B.ty = TApp { - ident = Global_ident.of_name Type Core__option__Option; + ident = Global_ident.of_name ~value:false Core__option__Option; args = [ GType result_typ ]; } in @@ -128,8 +128,7 @@ module%inlined_contents Make (F : Features.T) = struct | None -> (Core__option__Option__None, []) in MS.pat_PConstruct - ~constructor: - (Global_ident.of_name (Constructor { is_struct = false }) name) + ~constructor:(Global_ident.of_name ~value:true name) ~fields ~is_record:false ~is_struct:false ~typ:opt_result_typ in diff --git a/engine/lib/phases/phase_drop_return_break_continue.ml b/engine/lib/phases/phase_drop_return_break_continue.ml index ad0e6d201..00f3e3a34 100644 --- a/engine/lib/phases/phase_drop_return_break_continue.ml +++ b/engine/lib/phases/phase_drop_return_break_continue.ml @@ -152,7 +152,7 @@ module%inlined_contents Make (F : Features.T) = struct match body.typ with | TApp { ident; args = [ GType _; GType continue_type ] } when Ast.Global_ident.equal ident - (Ast.Global_ident.of_name Type + (Ast.Global_ident.of_name ~value:false Core__ops__control_flow__ControlFlow) -> continue_type | _ -> body.typ diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml index 3855c1e12..a583cbc6e 100644 --- a/engine/lib/phases/phase_functionalize_loops.ml +++ b/engine/lib/phases/phase_functionalize_loops.ml @@ -211,7 +211,7 @@ struct let pat = dpat pat in let fn : B.expr = UB.make_closure [ bpat; pat ] body body.span in let cf = Option.map ~f:fst control_flow in - let f, kind, args = + let f, args = match as_iterator it |> Option.bind ~f:(fn_args_of_iterator cf) with | Some (f, args, typ) -> (* TODO what happens if there is control flow? *) @@ -223,7 +223,7 @@ struct let pat, invariant = Option.value ~default invariant in UB.make_closure [ bpat; pat ] invariant invariant.span in - (f, Concrete_ident.Kind.Value, args @ [ invariant; init; fn ]) + (f, args @ [ invariant; init; fn ]) | None -> let fold : Concrete_ident.name = match cf with @@ -232,9 +232,9 @@ struct | Some BreakOnly -> Rust_primitives__hax__folds__fold_cf | None -> Core__iter__traits__iterator__Iterator__fold in - (fold, AssociatedItem Value, [ it; init; fn ]) + (fold, [ it; init; fn ]) in - UB.call ~kind f args span (dty span expr.typ) + UB.call f args span (dty span expr.typ) | Loop { body; @@ -276,8 +276,8 @@ struct | Some (BreakOnly, _) -> Rust_primitives__hax__while_loop_cf | None -> Rust_primitives__hax__while_loop in - UB.call ~kind:(AssociatedItem Value) fold_operator - [ condition; init; body ] span (dty span expr.typ) + UB.call fold_operator [ condition; init; body ] span + (dty span expr.typ) | Loop { state = None; _ } -> Error.unimplemented ~issue_id:405 ~details:"Loop without mutation" span diff --git a/engine/lib/phases/phase_reconstruct_asserts.ml b/engine/lib/phases/phase_reconstruct_asserts.ml index 0dfacd364..fe899c8b0 100644 --- a/engine/lib/phases/phase_reconstruct_asserts.ml +++ b/engine/lib/phases/phase_reconstruct_asserts.ml @@ -72,7 +72,7 @@ module Make (F : Features.T) = { e = GlobalVar - (Ast.Global_ident.of_name Value + (Ast.Global_ident.of_name ~value:true Core__ops__bit__Not__not); span = cond_expr.span; typ = TArrow ([ TBool ], TBool); @@ -94,7 +94,8 @@ module Make (F : Features.T) = { e = GlobalVar - (Ast.Global_ident.of_name Value Hax_lib__assert); + (Ast.Global_ident.of_name ~value:true + Hax_lib__assert); span = e.span; typ = TArrow diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml index d25841b05..2487644f4 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.ml +++ b/engine/lib/phases/phase_reconstruct_question_marks.ml @@ -71,7 +71,7 @@ module%inlined_contents Make (FA : Features.T) = struct (** Construct [Result] *) let make_result_type (success : ty) (error : ty) : ty = - let ident = Global_ident.of_name Type Core__result__Result in + let ident = Global_ident.of_name ~value:false Core__result__Result in TApp { ident; args = [ GType success; GType error ] } (** Retype a [Err::<_, E>(x)] literal, as [Err::(x)] *) @@ -92,8 +92,7 @@ module%inlined_contents Make (FA : Features.T) = struct else let from_typ = TArrow ([ error_src ], error_dest) in let from = - UA.call ~kind:(AssociatedItem Value) ~impl Core__convert__From__from - [] e.span from_typ + UA.call ~impl Core__convert__From__from [] e.span from_typ in let call = UA.call Core__result__Impl__map_err [ e; from ] e.span diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml index 22233e33a..b77977519 100644 --- a/engine/lib/phases/phase_simplify_question_marks.ml +++ b/engine/lib/phases/phase_simplify_question_marks.ml @@ -71,7 +71,7 @@ module%inlined_contents Make (FA : Features.T) = struct (** Construct [Result] *) let make_result_type (success : ty) (error : ty) : ty = - let ident = Global_ident.of_name Type Core__result__Result in + let ident = Global_ident.of_name ~value:false Core__result__Result in TApp { ident; args = [ GType success; GType error ] } (** Retype a [Err::<_, E>(x)] literal, as [Err::(x)] *) @@ -89,8 +89,8 @@ module%inlined_contents Make (FA : Features.T) = struct let from_typ = TArrow ([ error_src ], error_dest) in let impl_generic_args = [ GType error_dest; GType error_src ] in Some - (UA.call ~impl_generic_args ~kind:(AssociatedItem Value) ~impl - Core__convert__From__from [ e ] e.span from_typ) + (UA.call ~impl_generic_args ~impl Core__convert__From__from [ e ] + e.span from_typ) (** [map_err e error_dest impl] creates the expression [e.map_err(from)] with the proper types and impl @@ -99,10 +99,7 @@ module%inlined_contents Make (FA : Features.T) = struct let* success, error_src = expect_result_type e.typ in let* impl = expect_residual_impl_result impl in let from_typ = TArrow ([ error_src ], error_dest) in - let from = - UA.call ~kind:(AssociatedItem Value) ~impl Core__convert__From__from - [] e.span from_typ - in + let from = UA.call ~impl Core__convert__From__from [] e.span from_typ in let call = UA.call Core__result__Impl__map_err [ e; from ] e.span (make_result_type success error_dest) @@ -112,13 +109,11 @@ module%inlined_contents Make (FA : Features.T) = struct let mk_pconstruct ~is_struct ~is_record ~span ~typ (constructor : Concrete_ident_generated.t) (fields : (Concrete_ident_generated.t * pat) list) = - let constructor = - Global_ident.of_name (Constructor { is_struct }) constructor - in + let constructor = Global_ident.of_name ~value:true constructor in let fields = List.map ~f:(fun (field, pat) -> - let field = Global_ident.of_name Field field in + let field = Global_ident.of_name ~value:true field in { field; pat }) fields in diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml index 5b5f0a6b2..5916792c2 100644 --- a/engine/lib/phases/phase_specialize.ml +++ b/engine/lib/phases/phase_specialize.ml @@ -132,7 +132,7 @@ module Make (F : Features.T) = in match matching with | [ { fn_replace; _ } ] -> - let f = Ast.Global_ident.of_name Value fn_replace in + let f = Ast.Global_ident.of_name ~value:true fn_replace in let f = { f' with e = GlobalVar f } in { e with diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml index 6020266a4..f6159bd47 100644 --- a/engine/lib/phases/phase_traits_specs.ml +++ b/engine/lib/phases/phase_traits_specs.ml @@ -17,8 +17,7 @@ module Make (F : Features.T) = let ctx = Diagnostics.Context.Phase phase_id end) - let mk_name ident (kind : string) = - Concrete_ident.Create.map_last ~f:(fun s -> s ^ "_" ^ kind) ident + let mk_name ident kind = Concrete_ident.with_suffix kind ident module Attrs = Attr_payloads.Make (F) (Error) @@ -52,11 +51,11 @@ module Make (F : Features.T) = | TIFn (TArrow (inputs, output)) -> [ { - (mk Types.Requires "pre") with + (mk Types.Requires `Pre) with ti_v = TIFn (TArrow (inputs, TBool)); }; { - (mk Types.Ensures "post") with + (mk Types.Ensures `Post) with ti_v = TIFn (TArrow (inputs @ [ output ], TBool)); }; ] @@ -109,7 +108,7 @@ module Make (F : Features.T) = | Some (_, params, body) -> (params, body) | None -> (params, default) in - { (mk "pre") with ii_v = IIFn { body; params } }); + { (mk `Pre) with ii_v = IIFn { body; params } }); (let params, body = match Attrs.associated_fn Ensures item.ii_attrs with | Some (_, params, body) -> (params, body) @@ -136,7 +135,7 @@ module Make (F : Features.T) = in (params @ [ out ], default) in - { (mk "post") with ii_v = IIFn { body; params } }); + { (mk `Post) with ii_v = IIFn { body; params } }); ] | IIType _ -> [] in diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index a0ad06b81..858782a2a 100644 --- a/engine/lib/print_rust.ml +++ b/engine/lib/print_rust.ml @@ -2,11 +2,15 @@ open! Prelude open Ast open Ast.Full -module Concrete_ident_view = Concrete_ident.MakeViewAPI (struct - include Concrete_ident.DefaultNamePolicy +module View = struct + include Concrete_ident.MakeRenderAPI (struct + include Concrete_ident.DefaultNamePolicy - let index_field_transform field = "_" ^ field -end) + let anonymous_field_transform field = "_" ^ field + end) + + let to_definition_name id = (render id).name +end module AnnotatedString = struct module T = struct @@ -90,7 +94,7 @@ module Raw = struct let ( ! ) s = pure span (prefix ^ s) in match e with | `Concrete c -> - !(let s = Concrete_ident_view.show c in + !(let s = View.show c in if String.equal "_" s then "_anon" else s) | `Primitive p -> pprimitive_ident span p | `TupleType n -> ![%string "tuple%{Int.to_string n}"] @@ -126,7 +130,7 @@ module Raw = struct let rec last_of_global_ident (g : global_ident) span = match g with - | `Concrete c -> Concrete_ident_view.to_definition_name c + | `Concrete c -> View.to_definition_name c | `Projector c -> last_of_global_ident (c :> global_ident) span | _ -> Diagnostics.report @@ -169,7 +173,7 @@ module Raw = struct in !"arrow!(" & arrow & !")" | TAssociatedType _ -> !"proj_asso_type!()" - | TOpaque ident -> !(Concrete_ident_view.show ident) + | TOpaque ident -> !(View.show ident) | TDyn { goals; _ } -> let goals = concat ~sep:!" + " (List.map ~f:(pdyn_trait_goal span) goals) @@ -181,7 +185,7 @@ module Raw = struct let args = List.map ~f:(pgeneric_value span) non_self_args |> concat ~sep:!", " in - !(Concrete_ident_view.show trait) + !(View.show trait) & if List.is_empty args then empty else !"<" & args & !">" and pgeneric_value span (e : generic_value) : AnnotatedString.t = @@ -416,7 +420,7 @@ module Raw = struct let ptrait_goal span { trait; args } = let ( ! ) = pure span in let args = List.map ~f:(pgeneric_value span) args |> concat ~sep:!", " in - !(Concrete_ident_view.show trait) + !(View.show trait) & if List.is_empty args then empty else !"<" & args & !">" let pprojection_predicate span (pp : projection_predicate) = @@ -426,9 +430,9 @@ module Raw = struct |> Option.map ~f:(pty span) |> Option.value ~default:!"unknown_self" & !" :" - & !(Concrete_ident_view.show pp.impl.goal.trait) + & !(View.show pp.impl.goal.trait) & !"<" - & !(Concrete_ident_view.to_definition_name pp.assoc_item) + & !(View.to_definition_name pp.assoc_item) & !" = " & pty span pp.typ & !">" let pgeneric_constraint span (p : generic_constraint) = @@ -451,9 +455,7 @@ module Raw = struct !"{" & concat ~sep:!"," (List.map arguments ~f:(fun (id, ty, attrs) -> - pattrs attrs - & !(Concrete_ident_view.to_definition_name id) - & !":" & pty span ty)) + pattrs attrs & !(View.to_definition_name id) & !":" & pty span ty)) & !"}" else !"(" @@ -465,7 +467,7 @@ module Raw = struct let pvariant span (variant : variant) = let ( ! ) = pure span in pattrs variant.attrs - & !(Concrete_ident_view.to_definition_name variant.name) + & !(View.to_definition_name variant.name) & pvariant_body span variant let pvariants span variants = @@ -485,7 +487,7 @@ module Raw = struct let ( ! ) = pure ti.ti_span in let generics = pgeneric_params ti.ti_generics.params in let bounds = pgeneric_constraints ti.ti_span ti.ti_generics.constraints in - let ident = !(Concrete_ident_view.to_definition_name ti.ti_ident) in + let ident = !(View.to_definition_name ti.ti_ident) in pattrs ti.ti_attrs & match ti.ti_v with @@ -518,7 +520,7 @@ module Raw = struct let ( ! ) = pure span in let generics = pgeneric_params ii.ii_generics.params in let bounds = pgeneric_constraints span ii.ii_generics.constraints in - let ident = !(Concrete_ident_view.to_definition_name ii.ii_ident) in + let ident = !(View.to_definition_name ii.ii_ident) in pattrs ii.ii_attrs & match ii.ii_v with @@ -537,27 +539,27 @@ module Raw = struct | Fn { name; body; generics; params; safety } -> let return_type = pty e.span body.typ in (match safety with Safe -> !"fn " | Unsafe _ -> !"unsafe fn ") - & !(Concrete_ident_view.to_definition_name name) + & !(View.to_definition_name name) & pgeneric_params generics.params & pparams e.span params & !" -> " & return_type & pgeneric_constraints e.span generics.constraints & !"{" & pexpr body & !"}" | TyAlias { name; generics; ty } -> !"type " - & !(Concrete_ident_view.to_definition_name name) + & !(View.to_definition_name name) & pgeneric_params generics.params & pgeneric_constraints e.span generics.constraints & !"=" & pty e.span ty & !";" | Type { name; generics; variants = [ variant ]; is_struct = true } -> !"struct " - & !(Concrete_ident_view.to_definition_name name) + & !(View.to_definition_name name) & pgeneric_params generics.params & pgeneric_constraints e.span generics.constraints & pvariant_body e.span variant & if variant.is_record then !"" else !";" | Type { name; generics; variants; _ } -> !"enum " - & !(Concrete_ident_view.to_definition_name name) + & !(View.to_definition_name name) & pgeneric_params generics.params & pgeneric_constraints e.span generics.constraints & @@ -568,7 +570,7 @@ module Raw = struct match safety with Safe -> !"" | Unsafe _ -> !"unsafe " in safety & !"trait " - & !(Concrete_ident_view.to_definition_name name) + & !(View.to_definition_name name) & pgeneric_params generics.params & pgeneric_constraints e.span generics.constraints & !"{" diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml index c1e66f6dc..6ae966d42 100644 --- a/engine/lib/utils.ml +++ b/engine/lib/utils.ml @@ -25,6 +25,10 @@ let apply f x = f x let ( let* ) x f = Option.bind ~f x let some_if_true = function true -> Some () | _ -> None +let expect_singleton : 'a. 'a list -> 'a option = function + | [ x ] -> Some x + | _ -> None + (** [let*? () = guard in body] acts as a guard: if [guard] holds, then [body] is executed, otherwise [None] is returned. *) let ( let*? ) (type a) (x : bool) (f : unit -> a option) = @@ -51,6 +55,15 @@ let split_list ~equal ~needle (subject : 'a list) : 'a list list = in h subject +(** Map over a list with a option-returning function. Returns `Some` iff every calls to `f` returned `Some`. *) +let rec maybe_map ~(f : 'a -> 'b option) (l : 'a list) : 'b list option = + match l with + | hd :: tl -> + let* hd = f hd in + let* tl = maybe_map ~f tl in + Some (hd :: tl) + | [] -> Some [] + let first_letter s = String.prefix s 1 let is_uppercase s = String.equal s (String.uppercase s) let is_lowercase s = String.equal s (String.lowercase s) @@ -115,4 +128,22 @@ module List = struct let zip_opt : 'a 'b. 'a list -> 'b list -> ('a * 'b) list option = fun x y -> match zip x y with Ok result -> Some result | Unequal_lengths -> None + + let longest_prefix (type t) ~(eq : t -> t -> bool) (l : t list list) : t list + = + match l with + | [] -> [] + | hd :: tl -> + let tl = ref tl in + let f x = + let exception Stop in + try + tl := + List.map !tl ~f:(function + | y :: tl when eq x y -> tl + | _ -> raise Stop); + true + with Stop -> false + in + List.take_while ~f hd end diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index 9df5efea9..af1ea0919 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -146,9 +146,8 @@ macro_rules! impl_arith { } } -impl_arith!(u128); -// impl_arith!(u8, u16, u32, u64, u128, usize); -// impl_arith!(i8, i16, i32, i64, i128, isize); +impl_arith!(u8, u16, u32, u64, u128, usize); +impl_arith!(i8, i16, i32, i64, i128, isize); fn offset() {} diff --git a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js index 92825b158..6decb4220 100644 --- a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js +++ b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js @@ -360,8 +360,12 @@ let is_type = { // return output; // }; -let export_record = (fields, path) => { - let record_expression = fields.map(([field, type], i) => { +let export_record = (fields, path, name) => { + let record_expression = fields.map(([field, type, _doc], i) => { + if (field == 'index' && name == 'def_id_contents') { + // This is a hack to always parse Rust DefId indexes to `(0, 0)` + return 'index = Base.Int64.(zero, zero)'; + } let p = [...path, 'field_' + field]; let sub = mk_match('x', ocaml_arms_of_type_expr(type, p), p); let match = `match List.assoc_opt "${field}" l with Option.Some x -> begin ${sub} end | Option.None -> raise (MissingField {field = "${field}"; fields = l})`; @@ -402,7 +406,7 @@ let exporters = { ]; return ({ record: () => { - let [pat, expr] = export_record(Object.entries(payload), ['rec-variant_' + variant + '_' + variant_name]); + let [pat, expr] = export_record(Object.entries(payload), ['rec-variant_' + variant + '_' + variant_name], name); return wrap([[pat, variant + ' ' + expr]]); }, expr: () => wrap(ocaml_arms_of_type_expr(payload, ['expr-variant(PA):' + name + ':' + variant + ':' + variant_name]), variant + ' '), @@ -456,7 +460,7 @@ let exporters = { ([name, prop]) => [name, is_type.expr(prop), prop.description] ); - let [pat, expr] = export_record(fields, ['struct_' + name]); + let [pat, expr] = export_record(fields, ['struct_' + name], name); return { type: `{ ${fields.map(([fname, type, doc]) => `${fieldNameOf(fname)} : ${ocaml_of_type_expr(type, ['struct_' + fname + '_' + name])}${mkdoc(doc)}`).join(';\n')} }`, @@ -646,23 +650,23 @@ let table_id_node_of_yojson (type t) (name: string) (encode: t -> map_types) (de ).join('\nand ')); impl += ` and node_for__ty_kind_of_yojson (o: Yojson.Safe.t): node_for__ty_kind = - let (value, id) = + let (value, _id) = table_id_node_of_yojson "TyKind" (fun value -> \`TyKind value) (function | \`TyKind value -> Some value | _ -> None) ty_kind_of_yojson o in - {value; id} + {value; id = Base.Int64.zero} and node_for__def_id_contents_of_yojson (o: Yojson.Safe.t): node_for__def_id_contents = - let (value, id) = + let (value, _id) = table_id_node_of_yojson "DefIdContents" (fun value -> \`DefIdContents value) (function | \`DefIdContents value -> Some value | _ -> None) def_id_contents_of_yojson o in - {value; id} + {value; id = Base.Int64.zero} `; impl += (''); impl += ('let rec ' + items.map(({ name, type, parse, to_json }) => diff --git a/flake.nix b/flake.nix index 2bd83b20f..7f816698a 100644 --- a/flake.nix +++ b/flake.nix @@ -199,8 +199,9 @@ pkgs.rust-analyzer pkgs.toml2json rustfmt - rustc utils + + pkgs.rustup ]; LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; in {