diff --git a/engine/default.nix b/engine/default.nix index 1a676c743..e0505daa8 100644 --- a/engine/default.nix +++ b/engine/default.nix @@ -57,6 +57,7 @@ ppx_matches ppx_let ppx_enumerate + ppx_map cmdliner angstrom ppx_string diff --git a/engine/lib/analyses/concrete_ident_fresh_ns.ml b/engine/lib/analyses/concrete_ident_fresh_ns.ml new file mode 100644 index 000000000..010bb3fec --- /dev/null +++ b/engine/lib/analyses/concrete_ident_fresh_ns.ml @@ -0,0 +1,96 @@ +open! Prelude +module DefId = Concrete_ident_defid +open Concrete_ident_view + +module T = struct + type t = { id : int; path_hints : DefId.t list; name_hints : string list } + [@@deriving show, yojson, hash, compare, sexp, hash, eq] +end + +include T + +let make = + let state = ref 0 in + fun (path_hints : DefId.t list) (name_hints : string list) -> + state := !state + 1; + { id = !state; path_hints; name_hints } + +module Path = struct + module T = struct + type t = disambiguated_string list [@@deriving eq, compare, sexp, hash] + end + + include T + include Comparator.Make (T) +end + +(** A map from fresh namespace ids to view paths *) +let per_ns : + ( int, + (Path.t, _) Prelude.Set.t * disambiguated_string list option ) + Hashtbl.t = + Hashtbl.create (module Int) + +let register (ns : t) (did : DefId.t) = + let default : (_, Path.comparator_witness) Set.t * _ option = + (Set.empty (module Path), None) + in + Hashtbl.update per_ns ns.id + ~f: + ( Option.value ~default >> fun (set, opt) -> + let path = (of_def_id did).path in + (Set.add set path, opt) ) + +let get_path (ns : t) : disambiguated_string list = + let f paths = + let prefix = + Set.to_list paths + |> List.longest_prefix ~eq:[%equal: disambiguated_string] + in + let chunks = + Sequence.append + (Sequence.of_list + (prefix + @ List.concat_map + ~f:(fun did -> + (of_def_id did).path |> List.last |> Option.to_list) + ns.path_hints + @ List.map + ~f:(fun data -> + Concrete_ident_view.{ disambiguator = Int64.zero; data }) + ns.name_hints)) + (Sequence.unfold ~init:0 ~f:(fun id -> + Some + ( Concrete_ident_view. + { + disambiguator = Int64.of_int id; + data = "hax_" ^ Int.to_string ns.id ^ "_fresh_ns"; + }, + id + 1 ))) + in + let all_paths = + DefId.list_all () |> List.map ~f:(fun x -> (of_def_id x).path) |> ref + in + Sequence.take_while + (Sequence.mapi ~f:(fun i n -> (Int.equal i 0, n)) chunks) + ~f:(fun (is_first, chunk) -> + let remaining = + List.filter_map + ~f:(function + | hd :: tl when [%equal: disambiguated_string] hd chunk -> Some tl + | _ -> None) + !all_paths + in + all_paths := remaining; + (not (List.is_empty remaining)) || is_first) + |> Sequence.map ~f:snd |> Sequence.to_list + in + Hashtbl.update_and_return per_ns ns.id + ~f: + ( Option.value ~default:(Set.empty (module Path), None) + >> fun (paths, alloc) -> + ( paths, + alloc + |> Option.value_or_thunk ~default:(fun () -> f paths) + |> Option.some ) ) + |> snd |> Option.value_exn diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index b0d0cc160..8f6a59504 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -1,649 +1,198 @@ open! Prelude +module DefId = Concrete_ident_defid +module View = Concrete_ident_view +module FreshNamespace = Concrete_ident_fresh_ns -module Imported = struct - type def_id = { krate : string; path : path } - and path = disambiguated_def_path_item list +type reserved_suffix = [ `Cast | `Pre | `Post ] +[@@deriving show, yojson, hash, compare, sexp, hash, eq] - and disambiguated_def_path_item = { - data : def_path_item; - disambiguator : int; +module T = struct + type t = { + def_id : DefId.t; + moved : FreshNamespace.t option; + suffix : reserved_suffix option; } - - 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 } - - let impl { impl_prefix; impl_chunk; _ } = - { impl_prefix with path = impl_prefix.path @ [ impl_chunk ] } - - let path_decomposition - { impl_prefix = { path = prefix; _ }; impl_chunk; relative_path } = - (prefix, impl_chunk, relative_path) - end + [@@deriving show, yojson, hash, compare, sexp, hash, eq] + (** A `DefId` moved under a fresh namespace *) end -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 +include T +include Comparator.Make (T) -(** 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 +let to_debug_string = T.show - 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. - *) -end = struct - let state : (Imported.def_id, ImplInfos.t) Hashtbl.t option ref = ref None +let fresh_namespace (path_hints : t list) (string_hints : string list) : + FreshNamespace.t = + let path_hints = + List.concat_map + ~f:(fun { def_id; moved; _ } -> + def_id + :: (Option.to_list moved + |> List.concat_map ~f:(fun ns -> ns.FreshNamespace.path_hints))) + path_hints + in + FreshNamespace.make path_hints string_hints - module T = struct - type t = Imported.def_id [@@deriving show, yojson, compare, sexp, eq, hash] - end +module Cache = struct + let state = Hash_set.create (module T) + let cached = Fn.id &&& Hash_set.add state >> fst +end - 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 make (def_id : DefId.t) (moved : FreshNamespace.t option) + (suffix : reserved_suffix option) = + { def_id; moved; suffix } - let get_state () = - match !state with - | None -> failwith "ImplInfoStore was not initialized" - | Some state -> state +let of_def_id ?(suffix : reserved_suffix option = None) (kind : DefId.kind) + (def_id : Types.def_id) = + make (DefId.make kind def_id) None suffix |> Cache.cached - let find k = Hashtbl.find (get_state ()) k +let move_to_fresh_namespace (i : t) (ns : FreshNamespace.t) = + FreshNamespace.register ns i.def_id; + { i with moved = Some ns } |> Cache.cached - 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) -end +let with_suffix (suffix : reserved_suffix) (i : t) : t = + { i with suffix = Some suffix } -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 +module type VIEW_RENDERER = sig + val render_module : View.disambiguated_string -> string + val render_name : View.Name.t list -> string + val finalize : Concrete_ident_render_sig.rendered -> string end -module View = struct - module T = struct - type view = { crate : string; path : string list; definition : string } - end - - include T - - 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 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 MakeToString (R : VIEW_RENDERER) = struct + open Concrete_ident_render_sig - open Utils + let render (i : t) : rendered = + let Concrete_ident_view.{ path; name_path } = View.of_def_id i.def_id in + let path = List.map ~f:R.render_module path in + let name = R.render_name name_path in + { path; name } - 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 show (i : t) : string = + let { path; name } = render i 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 + match i.moved with + | Some ns -> FreshNamespace.get_path ns |> List.map ~f:R.render_module + | _ -> path in - let subst_dpi = - string_of_disambiguated_def_path_item >> Option.map ~f:subst + let name = + match i.suffix with + | Some suffix -> ( + name ^ "_" + ^ + match suffix with + | `Pre -> "pre" + | `Post -> "post" + | `Cast -> "cast_to_repr") + | _ -> name 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 } - - and to_definition_name x = (to_view x).definition + R.finalize { path; name } end -module T = struct - type t = { def_id : Imported.def_id; kind : Kind.t } - [@@deriving show, yojson, sexp] - - (* [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 +include Concrete_ident_render_sig.Make (T) - type name = Concrete_ident_generated.t - [@@deriving show, yojson, compare, sexp, eq, hash] +module MakeViewAPI (NP : NAME_POLICY) : RENDER_API = struct + open Concrete_ident_render_sig - let of_name k = Concrete_ident_generated.def_id_of >> of_def_id k + module R : VIEW_RENDERER = struct + let escape_sep = + let re = Re.Pcre.regexp "_(e*)_" in + let f group = "_e" ^ Re.Group.get group 1 ^ "_" in + Re.replace ~all:true re ~f - let eq_name name id = - let of_name = - Concrete_ident_generated.def_id_of name |> Imported.of_def_id - in - [%equal: Imported.def_id] of_name id.def_id -end + let sep = List.map ~f:escape_sep >> String.concat ~sep:"__" -include T -include View.T -include (val Comparator.make ~compare ~sexp_of_t) - -include Concrete_ident_sig.Make (struct - type t_ = t - type view_ = view -end) - -module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct - type t = T.t - - 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 + 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 - 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 }; - } - in - View.{ crate; path; definition = "discriminant_" ^ definition } - | _ -> to_view' { def_id; kind } - - and to_definition_name (x : t) : string = (to_view x).definition - - let to_crate_name (x : t) : string = (to_view x).crate - - let to_namespace x = - let View.{ crate; path; _ } = to_view x in - (crate, path) - - let show x = - to_view x - |> (fun View.{ crate; path; definition } -> - crate :: (path @ [ definition ])) - |> String.concat ~sep:"::" - - let local_ident (li : Local_ident.t) = + + let render_disambiguated View.{ disambiguator; data } = + if Int64.equal Int64.zero disambiguator then disambiguator_escape data + else data ^ "_" ^ Int64.to_string disambiguator + + let render_module = render_disambiguated + + type extn = [ View.Name.t | `Type of View.disambiguated_string ] + + let disambiguate_name (n : View.Name.t) : (string, string) View.Name.poly = + View.Name.add_strings n + |> View.Name.map_poly render_disambiguated render_disambiguated + + let rec render_name_plain : View.Name.t -> string = + View.Name.(disambiguate_name >> collect) >> sep + + let ( ^: ) x y = if String.is_empty x then y else sep [ x; y ] + + let rec render_last (prefix : string) (n : View.Name.t) : string = + match n with + | `AssociatedItem (item, (`Impl (_, `Inherent) as parent)) -> + let trait = render_name_plain (parent :> Name.View.t) in + let name = render_name_plain (item :> extn) in + let s = prefix ^: trait ^: name in + (* (match ) + *) failwith "" + | `Impl (_, _) -> prefix ^: render_name_plain (n :> extn) + | _ -> failwith "" + + let render_name = failwith "" + let finalize = failwith "" + end + + include MakeToString (R) + + let pp fmt = T.show >> Stdlib.Format.pp_print_string fmt + + let show id = + let { path; name } = render id in + path @ [ name ] |> String.concat ~sep:"::" + + 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 [ `Fn View.{ disambiguator = Int64.zero; data = li.name } ] end -let to_debug_string = T.show +(** 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 -let map_path_strings ~(f : string -> string) (cid : t) : t = - { cid with def_id = Imported.map_path_strings ~f cid.def_id } + module T = struct + type t = Types.def_id_contents [@@deriving show, compare, sexp, eq, hash] + end -module DefaultNamePolicy = 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 -end + let init impl_infos = + state := + impl_infos + |> Hashtbl.of_alist_multi (module T) + |> Hashtbl.map ~f:List.hd_exn |> Option.some -let matches_namespace (ns : Types.namespace) (did : t) : bool = - let did = 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)) - in - let rec aux (pattern : Types.namespace_chunk list) (path : string option list) - = - match (pattern, path) with - | [], [] -> true - | Exact x :: pattern, Some y :: path -> - [%equal: string] x y && aux pattern path - | Glob One :: pattern, _ :: path -> aux pattern path - | Glob Many :: pattern, [] -> aux pattern [] - | Glob Many :: pattern', _ :: path' -> - aux pattern' path || aux pattern path' - | _ -> 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 - let parent = parent id in - { - kind = Kind.Value; - def_id = - { - parent.def_id with - path = - parent.def_id.path - @ [ - { - data = TypeNs "rec_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 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 constructor name = - let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in - { name with def_id = { name.def_id with path } } + let lookup_raw (impl : t) : Types.impl_infos option = + find (DefId.def_id impl.def_id) end -let lookup_raw_impl_info (impl : t) : Types.impl_infos option = - ImplInfoStore.find impl.def_id +type name = Concrete_ident_generated.t +[@@deriving show, yojson, compare, sexp, eq, hash] -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 } +let of_name k = Concrete_ident_generated.def_id_of >> of_def_id k -module DefaultViewAPI = MakeViewAPI (DefaultNamePolicy) -include DefaultViewAPI +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 + (DefId.def_id id.def_id) diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli index e87f71b22..75b03a2a9 100644 --- a/engine/lib/concrete_ident/concrete_ident.mli +++ b/engine/lib/concrete_ident/concrete_ident.mli @@ -1,76 +1,71 @@ +module FreshNamespace : module type of Concrete_ident_fresh_ns + type t [@@deriving show, yojson, compare, sexp, eq, hash] type name = Concrete_ident_generated.t [@@deriving show, yojson, compare, sexp, eq, hash] -module ImplInfoStore : sig - val init : (Types.def_id * Types.impl_infos) list -> unit -end +type reserved_suffix = [ `Cast | `Pre | `Post ] +[@@deriving show, yojson, hash, compare, sexp, hash, eq] -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 +val of_def_id : + ?suffix:reserved_suffix option -> + Concrete_ident_defid.kind -> + Types.def_id -> + t -val of_def_id : Kind.t -> Types.def_id -> t -val of_name : Kind.t -> name -> t +val of_name : Concrete_ident_defid.kind -> name -> t val eq_name : name -> t -> bool val to_debug_string : t -> string +val fresh_namespace : t list -> string list -> FreshNamespace.t +val move_to_fresh_namespace : t -> FreshNamespace.t -> t +val with_suffix : reserved_suffix -> t -> t -module Create : sig - val fresh_module : from:t list -> t - val move_under : new_parent:t -> t -> t +(* module Create : sig + val fresh_module : from:t list -> t + val move_under : new_parent:t -> t -> t - val constructor : t -> t - (** [constructor ident] adds a [Ctor] to [ident] - this allows to build a constructor from a variant name. *) + val constructor : t -> t + (** [constructor ident] adds a [Ctor] to [ident] + this allows to build a constructor from a variant name. *) - 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 *) -end + 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 *) + end *) -type view = { crate : string; path : string list; definition : string } +(* type view = { crate : string; path : string list; definition : string } -val map_path_strings : f:(string -> string) -> t -> t -val matches_namespace : Types.namespace -> t -> bool + val map_path_strings : f:(string -> string) -> t -> t + val matches_namespace : Types.namespace -> t -> bool -include module type of struct - include Concrete_ident_sig.Make (struct - type t_ = t - type view_ = view - end) -end + include module type of struct + include Concrete_ident_sig.Make (struct + type t_ = t + type view_ = view + end) + end -module MakeViewAPI (NP : NAME_POLICY) : VIEW_API -module DefaultNamePolicy : NAME_POLICY -module DefaultViewAPI : VIEW_API + module MakeViewAPI (NP : NAME_POLICY) : VIEW_API + module DefaultNamePolicy : NAME_POLICY + module DefaultViewAPI : VIEW_API *) 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`. - -[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. *) - -val parent_impl : t -> t option -(** Returns the identifier pointing to the parent `impl` block, if it -exists. *) +module ImplInfoStore : sig + val init : (Types.def_id_contents * 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/concrete_ident_defid.ml b/engine/lib/concrete_ident/concrete_ident_defid.ml new file mode 100644 index 000000000..3cf05a1af --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_defid.ml @@ -0,0 +1,41 @@ +open! Prelude + +(** Rust shares one same `DefId` for the constructor of a struct and the type of the struct. We disambiguate that by creating a separate identifier here. *) +type kind = Regular | StructConstructor +[@@deriving show, yojson, hash, compare, sexp, hash, eq] + +module T = struct + module Types = struct + include Types + + let def_id_contents_of_yojson = Types.parse_def_id_contents + let yojson_of_def_id_contents = Types.to_json_def_id_contents + end + + type t = { kind : kind; def_id : Types.def_id_contents } + [@@deriving show, yojson, hash, compare, sexp, hash, eq] +end + +include T + +let contents (did : Types.def_id) = did.contents.value +let parent' (did : Types.def_id_contents) = did.parent |> Option.map ~f:contents + +let parent (did : t) = + parent' did.def_id |> Option.map ~f:(fun def_id -> { kind = Regular; def_id }) + +let rec parents' (did : t) = + did :: (parent did |> Option.map ~f:parents' |> Option.value ~default:[]) + +let parents = parents' >> List.drop_last_exn +let make' kind (def_id : Types.def_id) = { kind; def_id = contents def_id } +let state = Hash_set.create (module T) + +let make kind def_id = + let did = make' kind def_id in + Hash_set.add state did; + did + +let def_id { def_id; _ } = def_id +let kind { kind; _ } = kind +let list_all () = Hash_set.to_list state diff --git a/engine/lib/concrete_ident/concrete_ident_defid.mli b/engine/lib/concrete_ident/concrete_ident_defid.mli new file mode 100644 index 000000000..4d21d5cd7 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_defid.mli @@ -0,0 +1,11 @@ +type kind = Regular | StructConstructor +[@@deriving show, yojson, hash, compare, sexp, hash, eq] + +type t [@@deriving show, yojson, hash, compare, sexp, hash, eq] + +val parent : t -> t option +val parents : t -> t list +val make : kind -> Types.def_id -> t +val def_id : t -> Types.def_id_contents +val kind : t -> kind +val list_all : unit -> t list diff --git a/engine/lib/concrete_ident/concrete_ident_old.ml b/engine/lib/concrete_ident/concrete_ident_old.ml new file mode 100644 index 000000000..b0d0cc160 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_old.ml @@ -0,0 +1,649 @@ +open! Prelude + +module Imported = struct + type def_id = { krate : string; path : path } + and path = disambiguated_def_path_item list + + and disambiguated_def_path_item = { + data : def_path_item; + disambiguator : int; + } + + 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 } + + let impl { impl_prefix; impl_chunk; _ } = + { impl_prefix with path = impl_prefix.path @ [ impl_chunk ] } + + let path_decomposition + { impl_prefix = { path = prefix; _ }; impl_chunk; relative_path } = + (prefix, impl_chunk, relative_path) + end +end + +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 + +(** 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. + *) +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 + + 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) +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 +end + +module View = struct + module T = struct + type view = { crate : string; path : string list; definition : string } + end + + include T + + 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 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 + + open Utils + + 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 } + + and to_definition_name x = (to_view x).definition +end + +module T = struct + type t = { def_id : Imported.def_id; kind : Kind.t } + [@@deriving show, yojson, sexp] + + (* [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 + + type name = Concrete_ident_generated.t + [@@deriving show, yojson, compare, sexp, eq, hash] + + let of_name k = Concrete_ident_generated.def_id_of >> of_def_id k + + let eq_name name id = + let of_name = + Concrete_ident_generated.def_id_of name |> Imported.of_def_id + in + [%equal: Imported.def_id] of_name id.def_id +end + +include T +include View.T +include (val Comparator.make ~compare ~sexp_of_t) + +include Concrete_ident_sig.Make (struct + type t_ = t + type view_ = view +end) + +module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct + type t = T.t + + 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 + | _ -> 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 + 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 }; + } + in + View.{ crate; path; definition = "discriminant_" ^ definition } + | _ -> to_view' { def_id; kind } + + and to_definition_name (x : t) : string = (to_view x).definition + + let to_crate_name (x : t) : string = (to_view x).crate + + let to_namespace x = + let View.{ crate; path; _ } = to_view x in + (crate, path) + + let show x = + to_view x + |> (fun View.{ crate; path; definition } -> + crate :: (path @ [ definition ])) + |> String.concat ~sep:"::" + + let local_ident (li : Local_ident.t) = + 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; + } +end + +let to_debug_string = T.show + +let map_path_strings ~(f : string -> string) (cid : t) : t = + { cid with def_id = Imported.map_path_strings ~f cid.def_id } + +module DefaultNamePolicy = 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 +end + +let matches_namespace (ns : Types.namespace) (did : t) : bool = + let did = 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)) + in + let rec aux (pattern : Types.namespace_chunk list) (path : string option list) + = + match (pattern, path) with + | [], [] -> true + | Exact x :: pattern, Some y :: path -> + [%equal: string] x y && aux pattern path + | Glob One :: pattern, _ :: path -> aux pattern path + | Glob Many :: pattern, [] -> aux pattern [] + | Glob Many :: pattern', _ :: path' -> + aux pattern' path || aux pattern path' + | _ -> 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 + let parent = parent id in + { + kind = Kind.Value; + def_id = + { + parent.def_id with + path = + parent.def_id.path + @ [ + { + data = TypeNs "rec_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 } } +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_old.mli b/engine/lib/concrete_ident/concrete_ident_old.mli new file mode 100644 index 000000000..e87f71b22 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_old.mli @@ -0,0 +1,76 @@ +type t [@@deriving show, yojson, compare, sexp, eq, hash] + +type name = Concrete_ident_generated.t +[@@deriving show, yojson, compare, sexp, eq, hash] + +module ImplInfoStore : sig + val init : (Types.def_id * Types.impl_infos) list -> unit +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 + +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 + +module Create : sig + val fresh_module : from:t list -> t + val move_under : new_parent:t -> t -> t + + val constructor : t -> t + (** [constructor ident] adds a [Ctor] to [ident] + this allows to build a constructor from a variant name. *) + + 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 *) +end + +type view = { crate : string; path : string list; definition : string } + +val map_path_strings : f:(string -> string) -> t -> t +val matches_namespace : Types.namespace -> t -> bool + +include module type of struct + include Concrete_ident_sig.Make (struct + type t_ = t + type view_ = view + end) +end + +module MakeViewAPI (NP : NAME_POLICY) : VIEW_API +module DefaultNamePolicy : NAME_POLICY +module DefaultViewAPI : VIEW_API + +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`. + +[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. *) + +val parent_impl : t -> t option +(** Returns the identifier pointing to the parent `impl` block, if it +exists. *) diff --git a/engine/lib/concrete_ident/concrete_ident_sig.ml b/engine/lib/concrete_ident/concrete_ident_render_sig.ml similarity index 70% rename from engine/lib/concrete_ident/concrete_ident_sig.ml rename to engine/lib/concrete_ident/concrete_ident_render_sig.ml index 09af4797a..2ed721c13 100644 --- a/engine/lib/concrete_ident/concrete_ident_sig.ml +++ b/engine/lib/concrete_ident/concrete_ident_render_sig.ml @@ -1,8 +1,9 @@ open! Prelude +type rendered = { path : string list; name : string } + module Make (T : sig - type t_ - type view_ + type t end) = struct open T @@ -20,13 +21,10 @@ struct 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 + 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_view.ml b/engine/lib/concrete_ident/concrete_ident_view.ml new file mode 100644 index 000000000..a9af4a650 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_view.ml @@ -0,0 +1,137 @@ +open! Prelude +include Concrete_ident_view_types + +module FromDefId = struct + module DefId = Concrete_ident_defid + + (** 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 : DefId.t) : t = + failwith + ("DefId: an invariant have been broken. Expected " ^ msg ^ ".\n\ndid=" + ^ [%show: int] 0) + + let assert_parent did = + DefId.parent did + |> Option.value_or_thunk ~default:(fun _ -> + broken_invariant "the DefId to have a parent" did) + + let assert_type_ns (did : DefId.t) = + match List.last_exn (DefId.def_id did).path with + | { data = TypeNs data; disambiguator } -> { data; disambiguator } + | _ -> broken_invariant "TypeNs" did + + let assert_macro_ns (did : DefId.t) = + match List.last_exn (DefId.def_id did).path with + | { data = MacroNs data; disambiguator } -> { data; disambiguator } + | _ -> broken_invariant "MacroNs" did + + let assert_value_ns (did : DefId.t) = + match List.last_exn (DefId.def_id did).path with + | { data = ValueNs data; disambiguator } -> { data; disambiguator } + | _ -> broken_invariant "ValueNs" did + + let rec poly : + 'n 'd. + into_n:(DefId.t -> disambiguated_string -> 'n) -> + into_d:(DefId.t -> Int64.t -> 'd) -> + DefId.t -> + ('n, 'd) Name.poly = + fun ~into_n ~into_d did -> + let poly = poly ~into_n ~into_d in + let mk_associated_item kind : ('n, 'd) Name.poly = + `AssociatedItem + ( kind, + match assert_parent did |> poly with + | (`Impl _ | `Trait _) as p -> p + | _ -> broken_invariant "Impl | 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 + match (DefId.def_id did).kind with + | Struct when [%matches? DefId.StructConstructor] (DefId.kind 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 "StandaloneTypeNs" parent ) + | AssocFn -> `Fn (assert_value_ns did) |> mk_associated_item + | AssocConst -> `Const (assert_value_ns did) |> mk_associated_item + | AssocTy -> `Type (assert_value_ns did) |> mk_associated_item + | Field -> + let constructor = + match assert_parent did |> poly with + | `Constructor _ as p -> p + | _ -> failwith "Expected a Variant or a Standalone" + in + `Field (assert_type_ns did, constructor) + | Trait -> `Trait (assert_type_ns did) + | 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 (DefId.def_id did).path with + | { data = AnonConst; disambiguator } -> into_d did disambiguator + | _ -> failwith "todo: invariant broken") + | Impl { of_trait } -> + `Impl + (match List.last_exn (DefId.def_id did).path with + | { data = Impl; disambiguator } -> + (into_d did disambiguator, if of_trait then `Trait else `Inherent) + | _ -> failwith "todo: invariant broken") + | OpaqueTy -> `Opaque (assert_type_ns did) + | _ -> failwith "x" + + let view_name : DefId.t -> Name.t = + poly ~into_n:(fun _ n -> n) ~into_d:(fun _ d -> d) + + let view_name_did : DefId.t -> _ Name.poly = + let mk x y = (x, y) in + poly ~into_n:mk ~into_d:mk + + let decompose (did : DefId.t) : t = + let ns_chunks, rest = + List.split_while + ~f: + ( DefId.def_id >> fun def_id -> + match def_id.kind with Mod -> true | _ -> false ) + (DefId.parents did |> List.rev) + in + let name_path = + let rec f ids = + match ids with + | [] -> [] + | last :: _ -> + let suffix = view_name_did last in + Name.map_poly snd snd suffix + :: (List.drop_while + ~f: + ([%eq: DefId.t] + (suffix |> Name.map_poly fst fst |> Name.root) + >> not) + ids + |> f) + in + f rest + in + let path : disambiguated_string list = + { data = (DefId.def_id did).krate; disambiguator = Int64.zero } + :: List.map + ~f:(fun (m : DefId.t) -> + match (DefId.def_id m).path |> List.last_exn with + | Types.{ disambiguator; data = TypeNs data } -> + { data; disambiguator } + | _ -> failwith "todo: cannot handle anything but TypeNs") + ns_chunks + in + { path; name_path } +end + +let of_def_id = FromDefId.decompose 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..a4808ca3e --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_view.mli @@ -0,0 +1,3 @@ +include module type of Concrete_ident_view_types + +val of_def_id : Concrete_ident_defid.t -> t 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..19fa4f0a1 --- /dev/null +++ b/engine/lib/concrete_ident/concrete_ident_view_types.ml @@ -0,0 +1,64 @@ +open! Prelude + +type disambiguator = Int64.t +[@@deriving show, hash, compare, sexp, hash, eq, map] + +type disambiguated_string = { disambiguator : disambiguator; data : string } +[@@deriving show, hash, compare, sexp, hash, eq, map] + +module Name = struct + type 'name type_definition = + [ `Enum of 'name | `Struct of 'name | `Union of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type 'name constructor = [ `Constructor of 'name * 'name type_definition ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type 'name maybe_associated = [ `Fn of 'name | `Const of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type 'name associated = [ 'name maybe_associated | `Type of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type ('name, 'disambiguator) assoc_parent = + [ `Impl of 'disambiguator * [ `Inherent | `Trait ] | `Trait of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type ('name, 'disambiguator) poly = + [ 'name type_definition + | 'name constructor + | 'name maybe_associated + | ('name, 'disambiguator) assoc_parent + | `Use of 'name + | `AnonConst of 'disambiguator + | `TraitAlias of 'name + | `Foreign of 'name + | `Opaque of 'name + | `Static of 'name + | `Macro of 'name + | `AssociatedItem of 'name associated * ('name, 'disambiguator) assoc_parent + | `Field of 'name * 'name constructor ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type t = (disambiguated_string, disambiguator) poly + + let add_strings ?(impl = "impl") ?(anon_const = "anon_const") (n : t) : + (disambiguated_string, disambiguated_string) poly = + let f disambiguator = { disambiguator; data = impl } in + match map_poly Fn.id f n with + | `AnonConst o -> `AnonConst { o with data = anon_const } + | n -> n + + let rec collect : 'a. ('a, 'a) poly -> 'a list = function + | `AnonConst n | `Impl (n, _) | `Use n | `TraitAlias n | `Foreign n -> [ n ] + | `Opaque n | `Static n | `Macro n | `Enum n | `Struct n | `Union n -> [ n ] + | `Fn n | `Const n | `Trait n -> [ n ] + | `AssociatedItem ((`Fn a | `Const a | `Type a), b) -> + a :: collect (b :> _ poly) + | `Constructor (a, b) -> a :: collect (b :> _ poly) + | `Field (a, b) -> a :: collect (b :> _ poly) + + let root : 'a. ('a, 'a) poly -> 'a = fun x -> collect x |> List.last_exn +end + +type t = { path : disambiguated_string list; name_path : Name.t list } diff --git a/engine/lib/concrete_ident/remove me b/engine/lib/concrete_ident/remove me new file mode 100644 index 000000000..304e500e9 --- /dev/null +++ b/engine/lib/concrete_ident/remove me @@ -0,0 +1,405 @@ + +module DefName = struct + type disambiguator = Int64.t + [@@deriving show, hash, compare, sexp, hash, eq, map] + + type 'name type_definition = + [ `Enum of 'name | `Struct of 'name | `Union of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type 'name constructor = [ `Constructor of 'name * 'name type_definition ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type 'name maybe_associated = [ `Fn of 'name | `Const of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type 'name associated = [ 'name maybe_associated | `Type of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type ('name, 'disambiguator) assoc_parent = + [ `Impl of 'disambiguator | `Trait of 'name ] + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type ('name, 'disambiguator) t = + [ 'name type_definition + | 'name constructor + | 'name maybe_associated + | ('name, 'disambiguator) assoc_parent + | `Use of 'name + | `GlobalAsm of 'name + | `Closure of 'name + | `AnonConst of 'disambiguator + | `TraitAlias of 'name + | `Foreign of 'name + | `Opaque of 'name + | `Static of 'name + | `Macro of 'name + | `AssociatedItem of 'name associated * ('name, 'disambiguator) assoc_parent + | `Field of 'name * 'name constructor ] + (* | `ForeignMod of 'name *) + (* | `ExternCrate of 'name *) + (* | `Mod of 'name *) + (* | `Lifetime of 'name *) + [@@deriving show, hash, compare, sexp, hash, eq, enumerate, map] + + type named = { disambiguator : disambiguator; data : string } + + let assert_parent did = + DefId.parent did + |> Option.value_exn + ~message:"Was expecting a DefId to have a parent, found none" + + let assert_type_ns (did : DefId.t) = + match List.last_exn did.def_id.path with + | { data = TypeNs data; disambiguator } -> { data; disambiguator } + | _ -> failwith "Broken invariant: not TypeNs" + + let assert_macro_ns (did : DefId.t) = + match List.last_exn did.def_id.path with + | { data = MacroNs data; disambiguator } -> { data; disambiguator } + | _ -> failwith "Broken invariant: not MacroNs" + + let assert_value_ns (did : DefId.t) = + match List.last_exn did.def_id.path with + | { data = ValueNs data; disambiguator } -> { data; disambiguator } + | _ -> failwith "Broken invariant: not ValueNs" + + let rec of_def_id (did : DefId.t) : (named, disambiguator) t = + let mk_associated_item kind : _ t = + let parent = assert_parent did |> of_def_id in + `AssociatedItem + ( kind, + match parent with + | (`Impl _ | `Trait _) as p -> p + | _ -> failwith "Invariant broken" ) + in + match did.def_id.kind with + | Struct when [%matches? DefId.StructConstructor] did.kind -> + let name = assert_type_ns did in + `Constructor (name, `Struct name) + | Variant | Ctor _ -> + let parent = assert_parent did |> of_def_id in + let name = assert_type_ns did in + `Constructor + ( name, + match parent with + | (`Enum _ | `Struct _ | `Union _) as p -> p + | _ -> failwith "expected StandaloneTypeNs" ) + | AssocFn -> + let name = assert_value_ns did in + mk_associated_item (`Fn name) + | AssocConst -> + let name = assert_value_ns did in + mk_associated_item (`Const name) + | AssocTy -> + let name = assert_value_ns did in + mk_associated_item (`Type name) + | Field -> + let name = assert_type_ns did in + let constructor = + match assert_parent did |> of_def_id with + | `Constructor _ as p -> p + | _ -> failwith "Expected a Variant or a Standalone" + in + `Field (name, constructor) + | Trait -> `Trait (assert_type_ns did) + | 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 did.def_id.path with + | { data = AnonConst; disambiguator } -> disambiguator + | _ -> failwith "todo: invariant broken") + | Impl _ -> + `Impl + (match List.last_exn did.def_id.path with + | { data = Impl; disambiguator } -> disambiguator + | _ -> failwith "todo: invariant broken") + | OpaqueTy -> `Opaque (assert_type_ns did) + | _ -> failwith "todo" +end + +module NamespaceRepr = struct + type string_policy = + | StartsWith of { + reserved_prefix : string; + or_case : [ `Uppercase | `Lowercase ] option; + } + | None + + type ('category, 'concat, 't) t = + | Name of 'category * 't + | Concat of + 'concat * ('category, 'concat, 't) t * ('category, 'concat, 't) t + + type ('cat, 'name, 'disambiguator, 'concat, 'o) of_defname_fun = + into:(string_policy -> 'name -> 'o) -> + empty:(string_policy -> 'disambiguator -> 'o) -> + ('name, 'disambiguator) DefName.t -> + ('cat, 'concat, 'o) t + + module type POLICY = sig + type namespace_category + type concat_scheme + + val of_defname : + 'name 'disambiguator 'o. + ( namespace_category, + 'name, + 'disambiguator, + concat_scheme, + 'o ) + of_defname_fun + + val concat : string list -> string + end + + module Rust = struct + type category = [ `Type | `Value | `Lifetime | `Macro | `Impl | `AnonConst ] + type concat_scheme = unit + + let rec of_defname : + 'n 'd 'o. (category, 'n, 'd, concat_scheme, 'o) of_defname_fun = + fun ~into ~empty d -> + match d with + | `Enum n | `Struct n | `Union n | `Trait n | `Opaque n -> + Name (`Type, into None n) + | `Fn n | `Const n | `Static n -> Name (`Value, into None n) + | `Impl d -> Name (`Impl, empty None d) + | `AnonConst d -> Name (`AnonConst, empty None d) + | `Constructor (n, tdef) when [%matches? `Struct _] tdef -> + Name (`Type, into None n) + | `Constructor (n, tdef) -> + Concat + ( (), + of_defname (tdef :> _ DefName.t) ~into ~empty, + Name (`Type, into None n) ) + | _ -> failwith "?" + end + + module Make (P : POLICY) = struct + let rust = + let names = DefName.all [ () ] [ () ] in + let names = + let fresh = + let count = ref 0 in + fun () -> + count := !count + 1; + !count + in + List.map ~f:(DefName.map fresh fresh) names + in + let tbl = Hashtbl.create (module Int) in + let rust = + let mktup x y = Hashtbl.add_exn tbl x in + List.map ~f:(Rust.of_defname ~into:mktup ~empty:mktup) names + in + let backend = + List.map ~f:(P.of_defname ~into:(fun p _ -> p) ~empty:Fn.id) names + in + 0 + end + + (* let of_def_name () *) +end + +(** Describes the suffix of a `DefId`. This denotes the shortest +relevant suffix for a DefId. A definition can be standalone (i.e. a +simple funciton), or associated to some structure (i.e. a field is +associated to a variant, a variant is associated to a type, a method +to a trait, etc.). *) +module DefIdSuffix = struct + type associated_item_kind = Fn | Const | Ty + [@@deriving show, hash, compare, sexp, hash, eq] + + (* def_path_item UNION def_kind *) + type 'a t' = + | Standalone of { + kind : + [ (* `Type of [`OpaqueTy | `Struct | `Enum | `Union | `TyAlias | `TyParam | `ForeignTy | `Mod | ` ] *) + (* | `Macro *) + (* | `Value of [ *) + (* | `SyntheticCoroutineBody *) + (* | `ConstParam *) + (* | `Closure ] *) + (* | `LifetimeParam *) + (* | `Trait *) + (* | `TraitAlias *) + (* | `Fn *) + (* | `Const *) + `ExternCrate + | `Use + | `ForeignMod + | `AnonConst + | `InlineConst + | `Impl + | `OpaqueTy + | `GlobalAsm + | `Static ]; + } + (** A simple standalone item: a non-assoc. function, a non-assoc. constant, a trait, an impl, a static, etc. *) + | AssociatedItem of { kind : associated_item_kind; standalone_parent : 'a } + (** An associated item: it has one standalone parent (a trait). *) + | Variant of { standalone_type : 'a; kind : [ `Struct | `Variant ] } + (** A variant, which has exactly one standalone parent (a type). *) + | Field of { variant : 'a; standalone_type : 'a } + (** A field, has one variant and one type. *) + [@@deriving show, hash, compare, sexp, hash, eq] + + type t = DefId.t t' [@@deriving show, hash, compare, sexp, hash, eq] + + let top_def_id (suffix : t) : DefId.t = + match suffix with + | Standalone did + | AssociatedItem { standalone_parent = did; _ } + | Variant { standalone_type = did; _ } + | Field { standalone_type = did; _ } -> + did + + let rec of_def_id (did : DefId.t) : t = + let assert_parent did = + DefId.parent did + |> Option.value_exn + ~message:"Was expecting a DefId to have a parent, found none" + in + let mk_associated_item kind = + AssociatedItem { kind; standalone_parent = assert_parent did } + in + match did.def_id.kind with + | Struct when [%matches? DefId.StructConstructor] did.kind -> + Variant { standalone_type = assert_parent did; kind = `Struct } + | Variant | Ctor _ -> + Variant { standalone_type = assert_parent did; kind = `Variant } + | AssocFn -> mk_associated_item Fn + | AssocConst -> mk_associated_item Const + | AssocTy -> mk_associated_item Ty + | Field -> + let parent = assert_parent did in + let variant, standalone_type = + match of_def_id parent with + | Variant { standalone_type } -> (parent, standalone_type) + | Standalone _ -> ({ parent with kind = StructConstructor }, parent) + | _ -> failwith "Expected a Variant or a Standalone" + in + Field { variant; standalone_type } + | Macro _ | SyntheticCoroutineBody | TyParam | ConstParam | LifetimeParam + | Closure | Mod | Union | Enum | Struct | Trait | TyAlias | ForeignTy + | TraitAlias | Fn | Const | ExternCrate | Use | ForeignMod | AnonConst + | InlineConst | Impl _ | OpaqueTy | GlobalAsm | Static _ -> + Standalone did +end + +module Ident = struct + type fresh_namespace = { + path_hints : DefId.t list; + name_hints : string list; + disambiguator_hint : int; + } + + type t = + | DefId of DefId.t + | MovedUnder of { ns : fresh_namespace } + (** A `DefId` moved under a fresh namespace *) +end + +module Decomposed = struct + type disambiguated_ns_chunk = { disambiguator : Int64.t; ns_chunk : string } + + type t = { + namespace : disambiguated_ns_chunk list; + suffixes : DefIdSuffix.t list; (** non empty *) + } + + let of_def_id (did : DefId.t) = + let ns_chunks, rest = + List.split_while + ~f:(fun { def_id; _ } -> + match def_id.kind with Mod -> true | _ -> false) + (DefId.parents did |> List.rev) + in + let suffixes = + let rec f ids = + match ids with + | [] -> [] + | last :: _ -> + let suffix = DefIdSuffix.of_def_id last in + suffix + :: (List.drop_while + ~f:([%eq: DefId.t] (DefIdSuffix.top_def_id suffix) >> not) + ids + |> f) + in + f rest + in + let namespace = + { ns_chunk = did.def_id.krate; disambiguator = Int64.zero } + :: List.map + ~f:(fun (m : DefId.t) -> + match m.def_id.path |> List.last_exn with + | Types.{ disambiguator; data = TypeNs ns_chunk } -> + { ns_chunk; disambiguator } + | _ -> failwith "todo: cannot handle anything but TypeNs") + ns_chunks + in + { namespace; suffixes } +end + +module View = struct + type t = { crate : string; path : string list; definition : string } +end + +include Concrete_ident_sig.Make (struct + type t_ = DefId.t + type view_ = View.t +end) + +(** +Rust has different spaces for names: types, values, lifetime, macros. +That means that a type and a value can have the same exact name, yet be different paths. +A module lives in the type namespace for instance. + +In the same time, the backend has namespaces as well. For instance, F* has a "namespace" per struct: we don't need to prefix fields with field names, there is a disambigation mechanism. + +Thus, we need to account both for Rust namespaces and Backend namespaces. + +A namespace shall be defined as: under path , +*) + +type fmt = { formated : string -> bool; format : string -> string } + +type policy = { + separator : string; + type_ns : fmt; + value_ns : fmt; + impl_ns : fmt; +} + +module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct + let prefixes = [ "t"; "C"; "v"; "f"; "i"; "discriminant" ] + + let escape s = + match String.lsplit2 ~on:'_' s with + | Some (prefix, _) when List.mem ~equal:String.equal prefixes prefix -> + String.prefix prefix 1 ^ s + | _ -> s + + let render_suffix (s : DefIdSuffix.t) = 0 + + let to_view (did : DefId.t) : View.t = + let Decomposed.{ namespace; suffixes } = Decomposed.of_def_id did in + failwith "todo" +end + +(* type subpath_namespace = Type (\** A type namespace *\) | Value *) + +(* (\** A format defines a string scheme and a way to coerce to the scheme. Property: `∀ s. formated (format s)`. *\) *) + +(* type suffixes_fmt = { typ : fmt; value : fmt } *) +(* (\** How to format *\) *) + +(* module type NAME_POLICY = sig *) +(* val format_mod_ns : fmt *) +(* (\* val *\) *) +(* end *) diff --git a/engine/lib/dune b/engine/lib/dune index 17a3db14d..a23d723e3 100644 --- a/engine/lib/dune +++ b/engine/lib/dune @@ -1,6 +1,18 @@ (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 + concrete_ident_fresh_ns + utils) (libraries yojson non_empty_list @@ -32,6 +44,7 @@ ppx_generate_features ppx_functor_application ppx_enumerate + ppx_deriving.map ppx_matches))) (include_subdirs unqualified) diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml index c1e66f6dc..fb43143f7 100644 --- a/engine/lib/utils.ml +++ b/engine/lib/utils.ml @@ -115,4 +115,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/profile.dump b/engine/profile.dump new file mode 100644 index 000000000..e69de29bb