feat(frontend/traits): propagate improvements in tests

cryspen · Jan 31, 2024 · 8d18742 · 8d18742
1 parent 181375f
commit 8d18742
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 0 deletions.
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -58,6 +58,29 @@ class t_Foo (v_Self: Type) = {
   f_method_f:v_Self -> Prims.unit
 }
 
+let closure_impl_expr
+      (#v_I: Type)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Marker.t_Sized v_I)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I)
+      (it: v_I)
+    : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global =
+  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_map it (fun x -> x)
+      <:
+      Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit))
+
+let closure_impl_expr_fngen
+      (#v_I #v_F: Type)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Marker.t_Sized v_I)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Sized v_F)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Iter.Traits.Iterator.t_Iterator v_I)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: Core.Ops.Function.t_FnMut v_F Prims.unit)
+      (it: v_I)
+      (f: v_F)
+    : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global =
+  Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_map it f
+      <:
+      Core.Iter.Adapters.Map.t_Map v_I v_F)
+
 let f
       (#v_T: Type)
       (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Marker.t_Sized v_T)

diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
@@ -48,3 +48,11 @@ impl<'a> Struct {
         x.bar()
     }
 }
+
+pub fn closure_impl_expr<I: Iterator<Item = ()>>(it: I) -> Vec<()> {
+    it.map(|x| x).collect()
+}
+
+pub fn closure_impl_expr_fngen<I: Iterator<Item = ()>, F: FnMut(()) -> ()>(it: I, f: F) -> Vec<()> {
+    it.map(f).collect()
+}