wip

engine/default.nix

@@ -6,8 +6,6 @@ let
     pname = "non_empty_list";
     version = "0.1";
     src = fetchzip {
-      url =
-        "https://github.com/johnyob/ocaml-non-empty-list/archive/refs/tags/${version}.zip";
       url =
         "https://github.com/johnyob/ocaml-non-empty-list/archive/refs/tags/${version}.zip";
       sha256 = "sha256-BJlEi0yG2DRT5vuU9ulucMD5MPFt9duWgcNO1YsigiA=";
@@ -22,14 +20,11 @@ let
     version = "0.1";
 
     src = fetchzip {
-      url =
-        "https://github.com/wrbs/ppx_matches/archive/refs/tags/${version}.zip";
       url =
         "https://github.com/wrbs/ppx_matches/archive/refs/tags/${version}.zip";
       sha256 = "sha256-nAmWF8MgW0odKkRiFcHGsvJyIxNHaZpnOlNPsef89Fo=";
     };
 
-    buildInputs = [ ocamlPackages.ppxlib ];
     buildInputs = [ ocamlPackages.ppxlib ];
     duneVersion = "3";
     minimalOCamlVersion = "4.04";
@@ -50,17 +45,6 @@ let
       "rs"
       "mld"
     ];
-    src = lib.sourceFilesBySuffices ./. [
-      ".ml"
-      ".mli"
-      ".js"
-      "dune"
-      "dune-js"
-      "dune-project"
-      "sh"
-      "rs"
-      "mld"
-    ];
     buildInputs = with ocamlPackages;
       [
         base
@@ -108,25 +92,19 @@ let
       find "$bin" -type f -exec remove-references-to -t ${ocamlPackages.ocaml} '{}' +
     '';
 
-    outputs = [ "out" "bin" "lib" ];
     outputs = [ "out" "bin" "lib" ];
     passthru = {
       docs = hax-engine.overrideAttrs (old: {
         name = "hax-engine-docs";
         nativeBuildInputs = old.nativeBuildInputs ++ [ ocamlPackages.odoc ];
         buildPhase = "dune build @doc";
-        nativeBuildInputs = old.nativeBuildInputs ++ [ ocamlPackages.odoc ];
-        buildPhase = "dune build @doc";
         installPhase = "cp -rf _build/default/_doc/_html $out";
         outputs = [ "out" ];
-        outputs = [ "out" ];
       });
       js = hax-engine.overrideAttrs (old: {
         name = "hax-engine.js";
         nativeBuildInputs = old.nativeBuildInputs ++ [ closurecompiler gnused ];
         outputs = [ "out" ];
-        nativeBuildInputs = old.nativeBuildInputs ++ [ closurecompiler gnused ];
-        outputs = [ "out" ];
         buildPhase = ''
           # Enable JS build
           sed -i "s/; (include dune-js)/(include dune-js)/g" bin/dune
@@ -144,4 +122,3 @@ let
     };
   };
 in hax-engine.overrideAttrs (_: { name = "hax-engine"; })
-in hax-engine.overrideAttrs (_: { name = "hax-engine"; })

engine/lib/concrete_ident/concrete_ident.ml

@@ -1,8 +1,6 @@
 open! Prelude
 module View = Concrete_ident_view
 
-(** This module provides the global concrete identifiers. *)
-
 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
@@ -121,7 +119,7 @@ module T = struct
     suffix : reserved_suffix option;
   }
   [@@deriving show, yojson, hash, compare, sexp, hash, eq]
-  (** A `DefId` moved under a fresh namespace *)
+  (** A concrete identifier is defined as a  *)
 end
 
 include T
@@ -164,7 +162,10 @@ let with_suffix (suffix : reserved_suffix) (i : t) : t =
 
 module type VIEW_RENDERER = sig
   val render_module : View.DisambiguatedString.t -> string
-  val render_name : View.RelPath.Chunk.t list -> string option
+
+  val render_name :
+    namespace:View.ModPath.t -> View.RelPath.Chunk.t list -> string option
+
   val finalize : Concrete_ident_render_sig.rendered -> string
 end
 
@@ -191,7 +192,7 @@ module MakeToString (R : VIEW_RENDERER) = struct
     let Concrete_ident_view.{ mod_path; rel_path } = to_view i in
     let path = List.map ~f:R.render_module mod_path in
     let name =
-      let* name = R.render_name rel_path in
+      let* name = R.render_name ~namespace:mod_path rel_path in
       let name =
         match i.suffix with
         | Some suffix -> (
@@ -259,6 +260,8 @@ module type NAME_POLICY = Concrete_ident_render_sig.NAME_POLICY
 module MakeViewAPI (NP : NAME_POLICY) : RENDER_API = struct
   open Concrete_ident_render_sig
 
+  let is_reserved_word : string -> bool = Hash_set.mem NP.reserved_words
+
   module R : VIEW_RENDERER = struct
     let escape_sep =
       let re = Re.Pcre.regexp "_(e*)_" in
@@ -315,23 +318,69 @@ module MakeViewAPI (NP : NAME_POLICY) : RENDER_API = struct
         =
       let is_prefix_upper = prefix |> first_letter |> is_uppercase in
       let is_s_upper = s |> first_letter |> is_uppercase in
-      if Bool.equal is_s_upper is_prefix_upper && not requiered_prefix then
-        escape_prefixes s
-      else prefix ^ "_" ^ s
-
-    let rec render_last (extra : string) (n : View.RelPath.Chunk.t) : string =
+      if
+        Bool.equal is_s_upper is_prefix_upper
+        && (not requiered_prefix)
+        && not (is_reserved_word s)
+      then escape_prefixes s
+      else prefix ^ if String.is_empty s then "" else "_" ^ s
+
+    let render_last ~namespace (extra : string) (n : View.RelPath.Chunk.t) :
+        string =
       let value_fmt = format "v" false in
+      let field_fmt = format "f" true in
       let type_fmt = format "t" true in
+      (* let render_last = render_last ~namespace in *)
       let constructor_fmt ?(force_prefix = false) = format "C" force_prefix in
       match n with
-      | `AssociatedItem (((`Type n | `Const n | `Fn n) as item), parent) -> (
+      | `AssociatedItem
+          ((`Type n | `Const n | `Fn n), (`Trait _ | `Impl (_, _, _))) ->
+          let name = render_disambiguated n in
+          extra ^: field_fmt name
+      (* | `AssociatedItem (((`Type n | `Const n | `Fn n) as item), parent) ->
           let impl = render_last extra (parent :> _ View.RelPath.Chunk.poly) in
           let name = render_disambiguated n in
-          let s = impl ^: name in
-          match item with `Type _ -> type_fmt s | _ -> value_fmt s)
-      | `Impl (d, _) ->
-          (* TODO! *)
-          format "impl" true (extra ^: Int64.to_string d)
+          let name =
+            match item with `Type _ -> type_fmt name | _ -> value_fmt name
+          in
+          impl ^ "__" ^ escape_sep name *)
+      | `Impl (d, _, impl_infos) ->
+          let identifier =
+            let* impl_infos = impl_infos in
+            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
+          in
+          let default =
+            if Int64.equal Int64.zero d then "" else Int64.to_string d
+          in
+          let name = identifier |> Option.value ~default in
+          let prefix = "impl" in
+          let prefix =
+            if Option.is_some identifier then prefix ^ "_" else prefix
+          in
+          format prefix true (extra ^: name)
       | `AnonConst d -> format "anon_const" true (extra ^: Int64.to_string d)
       | `Use d -> format "use" true (extra ^: Int64.to_string d)
       | `Foreign d -> format "foreign" true (extra ^: Int64.to_string d)
@@ -361,12 +410,12 @@ module MakeViewAPI (NP : NAME_POLICY) : RENDER_API = struct
           else constructor_fmt (type_name ^ "_" ^ render_disambiguated cons)
       | `Macro n | `Static n | `Fn n | `Const n ->
           value_fmt (extra ^: render_disambiguated n)
-      | `Field (n, _) -> value_fmt (extra ^: render_disambiguated n)
+      | `Field (n, _) -> field_fmt (extra ^: render_disambiguated n)
 
-    let render_name (n : View.RelPath.t) =
+    let render_name ~namespace (n : View.RelPath.t) =
       let* fake_path, name = last_init n in
       let extra = List.map ~f:render_name_plain fake_path |> sep in
-      Some (render_last extra name)
+      Some (render_last ~namespace extra name)
 
     let finalize { path; name } =
       let path = List.map ~f:(map_first_letter String.uppercase) path in
@@ -386,7 +435,7 @@ module MakeViewAPI (NP : NAME_POLICY) : RENDER_API = struct
   let local_ident (li : Local_ident.t) : string =
     if Local_ident.is_final li then li.name
     else
-      R.render_name
+      R.render_name ~namespace:[]
         [
           `Fn
             View.DisambiguatedString.
@@ -398,37 +447,9 @@ end
 (** 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
+  include Explicit_def_id.ImplInfoStore
 
-  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 : t) : Types.impl_infos option =
-    find (Explicit_def_id.to_def_id impl.def_id)
+  let lookup_raw (impl : t) : Types.impl_infos option = lookup_raw impl.def_id
 end
 
 type name = Concrete_ident_generated.t

engine/lib/concrete_ident/concrete_ident_view.ml

@@ -59,7 +59,7 @@ let rec poly :
   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
-    | Struct when Explicit_def_id.is_constructor did ->
+    | (Ctor (Struct, _) | Struct) when Explicit_def_id.is_constructor did ->
         let name = assert_type_ns did in
         `Constructor (name, `Struct name)
     | Variant | Ctor _ ->
@@ -98,7 +98,9 @@ let rec poly :
         `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)
+              ( 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

engine/lib/concrete_ident/concrete_ident_view_types.ml

@@ -110,7 +110,8 @@ module RelPath = struct
       otherwise, some PPX is broken...  *)
 
     and ('name, 'disambiguator) assoc_parent =
-      [ `Impl of 'disambiguator * [ `Inherent | `Trait ]
+      [ `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. *)
@@ -174,7 +175,7 @@ module RelPath = struct
       | `Opaque n
       | `GlobalAsm n
       | `AnonConst n
-      | `Impl (n, _)
+      | `Impl (n, _, _)
       | `Use n
       | `Foreign n ->
           [ `D n ]

engine/lib/concrete_ident/explicit_def_id.ml

@@ -1,13 +1,6 @@
 open! Prelude
 
 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 = { is_constructor : bool; def_id : Types.def_id_contents }
   [@@deriving show, yojson, hash, compare, sexp, hash, eq]
 end
@@ -85,3 +78,39 @@ let rec parents (did : t) =
 
 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

engine/lib/concrete_ident/explicit_def_id.mli

@@ -65,3 +65,19 @@ 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