remove more now-superfluous rewrites

FStarLang · Feb 24, 2025 · 74c9f81 · 74c9f81
1 parent 786d361
commit 74c9f81
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 7 deletions.
diff --git a/share/pulse/examples/parallel/ParallelFor.fst b/share/pulse/examples/parallel/ParallelFor.fst
@@ -484,9 +484,6 @@ fn rec h_for_task
             #(pledge emp_inames (pool_done p) (on_range post mid hi))
             (h_for_task p ((e /. 2.0R) /. 2.0R) pre post f mid hi);
 
-    rewrite each iname_list [] as emp_inames;
-    // ^FIXME should be automatic
-
     (* We get this complicated pledge emp_inames from the spawns above. We can
     massage it before even waiting. *)
     assert (pledge emp_inames (pool_done p) (pledge emp_inames (pool_done p) (on_range post lo mid)));

diff --git a/share/pulse/examples/parallel/TaskPool.Examples.fst b/share/pulse/examples/parallel/TaskPool.Examples.fst
@@ -38,7 +38,6 @@ fn qs (n:nat)
   spawn_ p (fun () -> qsc 3);
   spawn_ p (fun () -> qsc 4);
   teardown_pool p;
-  rewrite each iname_list [] as emp_inames; // fixme should be automatic
   redeem_pledge emp_inames (pool_done p) (qsv 1);
   redeem_pledge emp_inames (pool_done p) (qsv 2);
   redeem_pledge emp_inames (pool_done p) (qsv 3);
@@ -58,7 +57,6 @@ fn qs_joinpromises (n:nat)
   spawn_ p (fun () -> qsc 2);
   spawn_ p (fun () -> qsc 3);
   spawn_ p (fun () -> qsc 4);
-  rewrite each iname_list [] as emp_inames; // fixme should be automatic
   join_pledge #emp_inames #(pool_done p) (qsv 1) (qsv 2);
   join_pledge #emp_inames #(pool_done p) (qsv 3) (qsv 4);
   teardown_pool p;
@@ -91,7 +89,6 @@ fn qsh (n:nat)
   // also qs12 could spawn and join its tasks, it would clearly work
   spawn_ p (fun () -> qsc 3);
   spawn_ p (fun () -> qsc 4);
-  rewrite each iname_list [] as emp_inames; // fixme should be automatic
   teardown_pool p;
   redeem_pledge emp_inames (pool_done p) (qsv 1 ** qsv 2);
   redeem_pledge emp_inames (pool_done p) (qsv 3);
@@ -108,7 +105,6 @@ fn qs12_par (#e:perm) (p:pool)
   {
     spawn_ p (fun () -> qsc 1);
     spawn_ p (fun () -> qsc 2);
-    rewrite each iname_list [] as emp_inames; // fixme should be automatic
     ()
   }