Rebase in progress

cryspen · Nov 21, 2023 · bb5a757 · bb5a757
1 parent 1691697
commit bb5a757
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 13 deletions.
diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
@@ -43,7 +43,7 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
         match Attrs.status i.attrs with Included _ -> true | _ -> false)
       items
   in
-  let items = Deps.sort items in
+  (* let items = Deps.sort items in *) (* TODO: should keep order for non-dependent functions by default? *)
   let reports =
     List.concat_map
       ~f:(fun (item : Ast.Rust.item) ->

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -1057,11 +1057,7 @@ let c_trait_item (item : Thir.trait_item) : trait_item =
   let open (val make ~krate:item.owner_id.krate : EXPR) in
   let { params; constraints } = c_generics item.generics in
   (* TODO: see TODO in impl items *)
-  let ti_ident =
-    Concrete_ident.of_def_id
-      (match (item.kind : _) with Const _ -> Value | _ -> Field)
-      item.owner_id
-  in
+  let ti_ident = Concrete_ident.of_def_id Field item.owner_id in
   {
     ti_span = Span.of_thir item.span;
     ti_generics = { params; constraints };
@@ -1295,11 +1291,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
                         backend will see traits and impls as
                         records. See https://github.com/hacspec/hacspec-v2/issues/271. *)
                      let ii_ident =
-                       Concrete_ident.of_def_id
-                         (match (item.kind : _) with
-                         | Const _ -> Value
-                         | _ -> Field)
-                         item.owner_id
+                       Concrete_ident.of_def_id Field item.owner_id
                      in
                      {
                        ii_span = Span.of_thir item.span;

diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
@@ -256,8 +256,21 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
                         })
                         .map(|path| (apred, path))
                 }) else {
-                    return ImplExprAtom::Todo(format!("implsource::param \n\n{:#?}", self))
-                        .with_args(impl_exprs(s, &nested));
+                    return
+                        if predicates.is_empty() {
+                            ImplExprAtom::Concrete {
+                                id: s.owner_id().sinto(s),
+                                generics: Vec::new(),
+                            }
+                            // ImplExprAtom::LocalBound {
+                            //     clause_id: rand::random(), // TODO
+                            //     path: Vec::<search_clause::PathChunk>::new().sinto(s)
+                            // }
+                        }
+                        else {
+                            ImplExprAtom::Todo(format!("implsource::param \n\n{:#?}", self))
+                        }
+                        .with_args(impl_exprs(s, &nested))
                 };
                 if apred.is_extra_self_predicate {
                     if !path.is_empty() {