Merge pull request #478 from hacspec/fix-select-trait-candidate

fix(frontend): fix select_trait_candidate
cryspen · Feb 1, 2024 · 572fb6e · 572fb6e
2 parents 7754643 + 8d18742
commit 572fb6e
Show file tree

Hide file tree

Showing 6 changed files with 240 additions and 87 deletions.
diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
@@ -268,6 +268,9 @@ functor
       | ImplApp of { impl : impl_expr; args : impl_expr list }
       | Dyn of trait_ref
       | Builtin of trait_ref
+      | FnPointer of ty
+      (* The `IE` suffix is there because visitors conflicts...... *)
+      | ClosureIE of todo
 
     and trait_ref = { trait : concrete_ident; args : generic_value list }
 

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -922,25 +922,27 @@ end) : EXPR = struct
         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 } ->
+    | 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, { trait_ref; _ }) ->
+          | 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 { trait_ref; _ } ->
+          | Parent { predicate = { trait_ref; _ }; _ } ->
               let trait = c_trait_ref span trait_ref in
               Parent { impl; trait }
         in
         List.fold ~init ~f path
     | Dyn { trait } -> Dyn (c_trait_ref span trait)
     | SelfImpl -> Self
     | 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)
     | Todo str -> failwith @@ "impl_expr_atom: Todo " ^ str
 
   and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value

diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
@@ -69,6 +69,8 @@ struct
           }
     | Dyn tr -> Dyn (dtrait_ref span tr)
     | Builtin tr -> Builtin (dtrait_ref span tr)
+    | ClosureIE todo -> ClosureIE todo
+    | FnPointer ty -> FnPointer (dty span ty)
 
   and dgeneric_value (span : span) (generic_value : A.generic_value) :
       B.generic_value =