Merge branch 'main' into ocaml-spans-reviewable

Author: karthikbhargavan

engine/lib/concrete_ident/concrete_ident.ml

@@ -503,7 +503,7 @@ module MakeRenderAPI (NP : NAME_POLICY) : RENDER_API = struct
       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 ]; _ } ->
+      | Some { value = { 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

engine/lib/concrete_ident/thir_simple_types.ml

@@ -58,15 +58,16 @@ let to_string ~(namespace : View.ModPath.t) :
     | Float F32 -> Some "f32"
     | Float F64 -> Some "f64"
     | Tuple [] -> Some "unit"
-    | Adt { def_id; generic_args = []; _ } -> Option.map ~f:escape (adt def_id)
+    | Adt { value = { 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 ]; _ } ->
+    | Adt { value = { def_id; generic_args = [ Type arg ]; _ }; _ } ->
         let* adt = adt def_id in
         let* arg = arity1 arg in
         Some (apply adt arg)

engine/lib/import_thir.ml

@@ -11,6 +11,8 @@ module Thir = struct
   type generic_param_kind = generic_param_kind_for__decorated_for__expr_kind
   type trait_item = trait_item_for__decorated_for__expr_kind
   type ty = node_for__ty_kind
+  type item_ref = node_for__item_ref_contents
+  type trait_ref = item_ref
 end
 
 open! Prelude
@@ -505,38 +507,35 @@ end) : EXPR = struct
           let then_ = c_expr then' in
           let else_ = Option.map ~f:c_expr else_opt in
           If { cond; else_; then_ }
-      | Call
-          {
-            args;
-            fn_span = _;
-            trait;
-            from_hir_call = _;
-            fun';
-            ty = _;
-            generic_args;
-            bounds_impls;
-          } ->
-          let args = List.map ~f:c_expr args in
-          let bounds_impls = List.map ~f:(c_impl_expr e.span) bounds_impls in
-          let c_generic_values = List.map ~f:(c_generic_value e.span) in
-          let generic_args = c_generic_values generic_args in
-          let f =
-            let f = c_expr fun' in
-            match (trait, fun'.contents) with
-            | Some _, GlobalName { id; _ } ->
-                { f with e = GlobalVar (def_id ~value:true id) }
-            | _ -> f
+      | Call { args; fn_span = _; from_hir_call = _; fun'; ty = _ } -> (
+          let args =
+            if List.is_empty args then [ unit_expr span ]
+            else List.map ~f:c_expr args
           in
-          let args = if List.is_empty args then [ unit_expr span ] else args in
-          App
-            {
-              f;
-              args;
-              generic_args;
-              bounds_impls;
-              trait =
-                Option.map ~f:(c_impl_expr e.span *** c_generic_values) trait;
-            }
+          let f = c_expr fun' in
+          match fun'.contents with
+          | GlobalName
+              {
+                item =
+                  {
+                    value = { def_id = id; generic_args; impl_exprs; in_trait };
+                    _;
+                  };
+                _;
+              } ->
+              let f = { f with e = GlobalVar (def_id ~value:true id) } in
+              let bounds_impls = List.map ~f:(c_impl_expr e.span) impl_exprs in
+              let generic_args =
+                List.map ~f:(c_generic_value e.span) generic_args
+              in
+              let in_trait = Option.map ~f:(c_impl_expr e.span) in_trait in
+              let trait =
+                Option.map ~f:(fun ie -> (ie, ie.goal.args)) in_trait
+              in
+              App { f; args; generic_args; bounds_impls; trait }
+          | _ ->
+              App
+                { f; args; generic_args = []; bounds_impls = []; trait = None })
       | Box { value } ->
           (U.call Rust_primitives__hax__box_new [ c_expr value ] span typ).e
       | Deref { arg } ->
@@ -645,7 +644,9 @@ end) : EXPR = struct
               trait = None (* TODO: see issue #328 *);
               bounds_impls = [];
             }
-      | GlobalName { id; constructor = _ } -> GlobalVar (def_id ~value:true id)
+      | GlobalName { item = { value = { def_id = id; _ }; _ }; constructor = _ }
+        ->
+          GlobalVar (def_id ~value:true id)
       | UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident Expr id)
       | Borrow { arg; borrow_kind = kind } ->
           let e' = c_expr arg in
@@ -732,9 +733,14 @@ end) : EXPR = struct
                        typ = TInt { size = S8; signedness = Unsigned };
                      })
                    l))
-      | NamedConst { def_id = id; impl; args; _ } ->
+      | NamedConst
+          {
+            item =
+              { value = { def_id = id; generic_args; in_trait = impl; _ }; _ };
+            _;
+          } ->
           let f = GlobalVar (def_id ~value:true id) in
-          let args = List.map ~f:(c_generic_value e.span) args in
+          let args = List.map ~f:(c_generic_value e.span) generic_args in
           let const_args =
             List.filter_map args ~f:(function GConst e -> Some e | _ -> None)
           in
@@ -854,7 +860,7 @@ end) : EXPR = struct
           Array { fields = List.map ~f:constant_expr_to_expr fields }
       | Tuple { fields } ->
           Tuple { fields = List.map ~f:constant_expr_to_expr fields }
-      | GlobalName { id; _ } -> GlobalName { id; constructor = None }
+      | GlobalName item -> GlobalName { item; constructor = None }
       | Borrow arg ->
           Borrow { arg = constant_expr_to_expr arg; borrow_kind = Thir.Shared }
       | ConstRef { id } -> ConstRef { id }
@@ -1024,16 +1030,14 @@ end) : EXPR = struct
     | Float k ->
         TFloat
           (match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128)
-    | Arrow signature
-    | Closure (_, { untupled_sig = signature; _ })
-    | FnDef { fn_sig = signature; _ } ->
-        let ({ inputs; output; _ } : Thir.ty_fn_sig) = signature.value in
+    | Arrow fn_sig | Closure { fn_sig; _ } | FnDef { fn_sig; _ } ->
+        let ({ inputs; output; _ } : Thir.ty_fn_sig) = fn_sig.value in
         let inputs =
           if List.is_empty inputs then [ U.unit_typ ]
           else List.map ~f:(c_ty span) inputs
         in
         TArrow (inputs, c_ty span output)
-    | Adt { def_id = id; generic_args; _ } ->
+    | Adt { value = { def_id = id; generic_args; _ }; _ } ->
         let ident = def_id ~value:false id in
         let args = List.map ~f:(c_generic_value span) generic_args in
         TApp { ident; args }
@@ -1118,15 +1122,15 @@ end) : EXPR = struct
     let goal = c_trait_ref span ie.trait.value in
     let impl = { kind = c_impl_expr_atom span ie.impl; goal } in
     match ie.impl with
-    | Concrete { impl_exprs = []; _ } -> impl
-    | Concrete { impl_exprs; _ } ->
+    | Concrete { value = { impl_exprs = []; _ }; _ } -> impl
+    | Concrete { value = { impl_exprs; _ }; _ } ->
         let args = List.map ~f:(c_impl_expr span) impl_exprs in
         { kind = ImplApp { impl; args }; goal }
     | _ -> impl
 
   and c_trait_ref span (tr : Thir.trait_ref) : trait_goal =
-    let trait = Concrete_ident.of_def_id ~value:false tr.def_id in
-    let args = List.map ~f:(c_generic_value span) tr.generic_args in
+    let trait = Concrete_ident.of_def_id ~value:false tr.value.def_id in
+    let args = List.map ~f:(c_generic_value span) tr.value.generic_args in
     { trait; args }
 
   and c_impl_expr_atom (span : Thir.span) (ie : Thir.impl_expr_atom) :
@@ -1140,7 +1144,7 @@ end) : EXPR = struct
           let ident =
             { goal = c_trait_ref span trait_ref; name = predicate_id }
           in
-          let item = Concrete_ident.of_def_id ~value:false item.def_id in
+          let item = Concrete_ident.of_def_id ~value:false item.value.def_id in
           let trait_ref = c_trait_ref span trait_ref in
           Projection
             { impl = { kind = item_kind; goal = trait_ref }; ident; item }
@@ -1153,9 +1157,9 @@ end) : EXPR = struct
           Parent { impl = { kind = item_kind; goal = trait_ref }; ident }
     in
     match ie with
-    | Concrete { id; generics; _ } ->
-        let trait = Concrete_ident.of_def_id ~value:false id in
-        let args = List.map ~f:(c_generic_value span) generics in
+    | Concrete { value = { def_id; generic_args; _ }; _ } ->
+        let trait = Concrete_ident.of_def_id ~value:false def_id in
+        let args = List.map ~f:(c_generic_value span) generic_args in
         Concrete { trait; args }
     | LocalBound { predicate_id; path; _ } ->
         let init = LocalBound { id = predicate_id } in
@@ -1250,8 +1254,12 @@ end) : EXPR = struct
       generic_constraint option =
     match kind with
     | Trait { is_positive = true; trait_ref } ->
-        let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in
-        let trait = Concrete_ident.of_def_id ~value:false trait_ref.def_id in
+        let args =
+          List.map ~f:(c_generic_value span) trait_ref.value.generic_args
+        in
+        let trait =
+          Concrete_ident.of_def_id ~value:false trait_ref.value.def_id
+        in
         Some (GCType { goal = { trait; args }; name = id })
     | Projection { impl_expr; assoc_item; ty } ->
         let impl = c_impl_expr span impl_expr in
@@ -1330,7 +1338,7 @@ include struct
 
   let import_ty : Types.span -> Types.node_for__ty_kind -> Ast.Rust.ty = c_ty
 
-  let import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal =
+  let import_trait_ref : Types.span -> Thir.trait_ref -> Ast.Rust.trait_goal =
     c_trait_ref
 
   let import_clause :
@@ -1778,9 +1786,10 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
              generics = c_generics generics;
              self_ty = c_ty item.span self_ty;
              of_trait =
-               ( Concrete_ident.of_def_id ~value:false of_trait.def_id,
-                 List.map ~f:(c_generic_value item.span) of_trait.generic_args
-               );
+               ( Concrete_ident.of_def_id ~value:false of_trait.value.def_id,
+                 List.map
+                   ~f:(c_generic_value item.span)
+                   of_trait.value.generic_args );
              items;
              parent_bounds =
                List.filter_map

engine/lib/import_thir.mli

@@ -1,5 +1,7 @@
 val import_ty : Types.span -> Types.node_for__ty_kind -> Ast.Rust.ty
-val import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal
+
+val import_trait_ref :
+  Types.span -> Types.node_for__item_ref_contents -> Ast.Rust.trait_goal
 
 val import_clause :
   Types.span -> Types.clause -> Ast.Rust.generic_constraint option

engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js

@@ -591,6 +591,7 @@ end
     let items = Object.entries(definitions)
         .map(([name, def]) => ['Node_for_TyKind' == name ? 'node_for_ty_kind_generated' : name, def])
         .map(([name, def]) => ['Node_for_DefIdContents' == name ? 'node_for_def_id_contents_generated' : name, def])
+        .map(([name, def]) => ['Node_for_ItemRefContents' == name ? 'node_for_item_ref_contents_generated' : name, def])
         .map(
             ([name, def]) => export_definition(name, def)
         ).filter(x => x instanceof Object);
@@ -626,9 +627,10 @@ open ParseError
     impl += `
 and node_for__ty_kind = node_for_ty_kind_generated
 and node_for__def_id_contents = node_for_def_id_contents_generated
+and node_for__item_ref_contents = node_for_item_ref_contents_generated
 
 
-type map_types = ${"[`TyKind of ty_kind | `DefIdContents of def_id_contents]"}
+type map_types = ${"[`TyKind of ty_kind | `DefIdContents of def_id_contents | `ItemRefContents of item_ref_contents]"}
 let cache_map: (int64, ${"[ `Value of map_types | `JSON of Yojson.Safe.t ]"}) Base.Hashtbl.t = Base.Hashtbl.create (module Base.Int64)
 
 module Exn = struct
@@ -682,6 +684,15 @@ and node_for__def_id_contents_of_yojson (o: Yojson.Safe.t): node_for__def_id_con
            o
    in
    {value; id = Base.Int64.zero}
+and node_for__item_ref_contents_of_yojson (o: Yojson.Safe.t): node_for__item_ref_contents =
+   let (value, _id) =
+       table_id_node_of_yojson "ItemRefContents"
+           (fun value -> \`ItemRefContents value)
+           (function | \`ItemRefContents value -> Some value | _ -> None)
+           item_ref_contents_of_yojson
+           o
+   in
+   {value; id = Base.Int64.zero}
 `;
     impl += ('');
     impl += ('let rec ' + items.map(({ name, type, parse, to_json }) =>
@@ -690,6 +701,7 @@ and node_for__def_id_contents_of_yojson (o: Yojson.Safe.t): node_for__def_id_con
     impl += `
 and yojson_of_node_for__ty_kind {value; id} = yojson_of_node_for_ty_kind_generated {value; id}
 and yojson_of_node_for__def_id_contents {value; id} = yojson_of_node_for_def_id_contents_generated {value; id}
+and yojson_of_node_for__item_ref_contents {value; id} = yojson_of_node_for_item_ref_contents_generated {value; id}
 end
 
 open struct

frontend/exporter/src/constant_utils.rs

@@ -60,11 +60,7 @@ pub enum ConstantExprKind {
     ///
     /// If `options.inline_anon_consts` is `false`, this is also used for inline const blocks and
     /// advanced const generics expressions.
-    GlobalName {
-        id: GlobalIdent,
-        generics: Vec<GenericArg>,
-        trait_refs: Vec<ImplExpr>,
-    },
+    GlobalName(ItemRef),
     /// A trait constant
     ///
     /// Ex.:
@@ -94,19 +90,7 @@ pub enum ConstantExprKind {
     ConstRef {
         id: ParamConst,
     },
-    FnPtr {
-        def_id: DefId,
-        generics: Vec<GenericArg>,
-        /// The implementation expressions for every generic bounds
-        /// ```text
-        /// fn foo<T : Bar>(...)
-        ///            ^^^
-        /// ```
-        generics_impls: Vec<ImplExpr>,
-        /// If the function is a method of trait `Foo`, `method_impl`
-        /// is an implementation of `Foo`
-        method_impl: Option<ImplExpr>,
-    },
+    FnPtr(ItemRef),
     /// A blob of memory containing the byte representation of the value. This can occur when
     /// evaluating MIR constants. Interpreting this back to a structured value is left as an
     /// exercice to the consumer.
@@ -175,13 +159,8 @@ impl From<ConstantExpr> for Expr {
                 base: AdtExprBase::None,
                 user_ty: None,
             }),
-            // TODO: propagate the generics and trait refs (see #636)
-            GlobalName {
-                id,
-                generics: _,
-                trait_refs: _,
-            } => ExprKind::GlobalName {
-                id,
+            GlobalName(item) => ExprKind::GlobalName {
+                item,
                 constructor: None,
             },
             Borrow(e) => ExprKind::Borrow {