Merge pull request #487 from hacspec/fix-self-482

Frontend: fix `Self`
cryspen · Feb 1, 2024 · 80c7317 · 80c7317
2 parents 572fb6e + 4f8a78a
commit 80c7317
Show file tree

Hide file tree

Showing 4 changed files with 38 additions and 33 deletions.
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -917,29 +917,29 @@ end) : EXPR = struct
 
   and c_impl_expr_atom (span : Thir.span) (ie : Thir.impl_expr_atom) : impl_expr
       =
+    let browse_path (impl : impl_expr) (chunk : Thir.impl_expr_path_chunk) =
+      match chunk with
+      | AssocItem { item; predicate = { trait_ref; _ }; _ } ->
+          let trait = c_trait_ref span trait_ref in
+          let kind : Concrete_ident.Kind.t =
+            match item.kind with Const | Fn -> Value | Type -> Type
+          in
+          let item = Concrete_ident.of_def_id kind item.def_id in
+          Projection { impl; trait; item }
+      | Parent { predicate = { trait_ref; _ }; _ } ->
+          let trait = c_trait_ref span trait_ref in
+          Parent { impl; trait }
+    in
     match ie with
     | Concrete { id; generics } ->
         let trait = Concrete_ident.of_def_id Impl id in
         let args = List.map ~f:(c_generic_value span) generics in
         Concrete { trait; args }
     | LocalBound { clause_id; path; _ } ->
         let init = LocalBound { id = clause_id } in
-        let f (impl : impl_expr) (chunk : Thir.impl_expr_path_chunk) =
-          match chunk with
-          | AssocItem { item; predicate = { trait_ref; _ }; _ } ->
-              let trait = c_trait_ref span trait_ref in
-              let kind : Concrete_ident.Kind.t =
-                match item.kind with Const | Fn -> Value | Type -> Type
-              in
-              let item = Concrete_ident.of_def_id kind item.def_id in
-              Projection { impl; trait; item }
-          | Parent { predicate = { trait_ref; _ }; _ } ->
-              let trait = c_trait_ref span trait_ref in
-              Parent { impl; trait }
-        in
-        List.fold ~init ~f path
+        List.fold ~init ~f:browse_path path
     | Dyn { trait } -> Dyn (c_trait_ref span trait)
-    | SelfImpl -> Self
+    | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
     | Builtin { trait } -> Builtin (c_trait_ref span trait)
     | FnPointer { fn_ty } -> FnPointer (c_ty span fn_ty)
     | Closure _ as x -> ClosureIE ([%show: Thir.impl_expr_atom] x)

diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
@@ -30,7 +30,10 @@ pub enum ImplExprAtom {
         r#trait: Binder<TraitRef>,
         path: Vec<ImplExprPathChunk>,
     },
-    SelfImpl,
+    SelfImpl {
+        r#trait: Binder<TraitRef>,
+        path: Vec<ImplExprPathChunk>,
+    },
     /// `dyn TRAIT` is a wrapped value with a virtual table for trait
     /// `TRAIT`.  In other words, a value `dyn TRAIT` is a dependent
     /// triple that gathers a type τ, a value of type τ and an
@@ -313,25 +316,21 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
                     })
                 };
                 use rustc_middle::ty::ToPolyTraitRef;
+                let r#trait = apred
+                    .predicate
+                    .to_opt_poly_trait_pred()
+                    .s_unwrap(s)
+                    .to_poly_trait_ref()
+                    .sinto(s);
+                let path = path.sinto(s);
                 if apred.is_extra_self_predicate {
-                    if !path.is_empty() {
-                        supposely_unreachable_fatal!(s[apred.span], "SelfWithNonEmptyPath"; {
-                            self, apred, path
-                        });
-                    }
-                    ImplExprAtom::SelfImpl.with_args(vec![], trait_ref)
+                    ImplExprAtom::SelfImpl { r#trait, path }
+                        .with_args(impl_exprs(s, &nested), trait_ref)
                 } else {
-                    let clause_id: u64 = clause_id_of_predicate(apred.predicate);
-                    let r#trait = apred
-                        .predicate
-                        .to_opt_poly_trait_pred()
-                        .s_unwrap(s)
-                        .to_poly_trait_ref()
-                        .sinto(s);
                     ImplExprAtom::LocalBound {
-                        clause_id,
+                        clause_id: clause_id_of_predicate(apred.predicate),
                         r#trait,
-                        path: path.sinto(s),
+                        path,
                     }
                     .with_args(impl_exprs(s, &nested), trait_ref)
                 }

diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -55,7 +55,8 @@ class t_Foo (v_Self: Type) = {
   f_AssocType:Core.Marker.t_Sized _;
   f_N:usize;
   f_assoc_f:Prims.unit -> Prims.unit;
-  f_method_f:v_Self -> Prims.unit
+  f_method_f:v_Self -> Prims.unit;
+  f_assoc_type:{| i3: Core.Marker.t_Copy _ |} -> _ -> Prims.unit
 }
 
 let closure_impl_expr
@@ -103,7 +104,8 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit =
     f_AssocType = i32;
     f_N = sz 32;
     f_assoc_f = () <: Prims.unit;
-    f_method_f = fun (self: Prims.unit) -> f_assoc_f ()
+    f_method_f = (fun (self: Prims.unit) -> f_assoc_f ());
+    f_assoc_type = fun (_: i32) -> ()
   }
 
 type t_Struct = | Struct : t_Struct

diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
@@ -9,6 +9,9 @@ pub trait Foo {
     const N: usize;
     fn assoc_f() -> ();
     fn method_f(&self) -> ();
+    fn assoc_type(_: Self::AssocType) -> ()
+    where
+        Self::AssocType: Copy;
 }
 
 impl SuperTrait for i32 {
@@ -26,6 +29,7 @@ impl Foo for () {
     fn method_f(&self) {
         Self::assoc_f()
     }
+    fn assoc_type(_: Self::AssocType) -> () {}
 }
 
 fn f<T: Foo>(x: T) {