From d4ad01177c5f7d224e1e2811642b3fbbccb770bf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Feb 2025 16:36:29 +0000 Subject: [PATCH] Update the way we compute which functions should be reducible --- src/pure/PureMicroPasses.ml | 25 +++++-------------------- tests/lean/Arrays.lean | 4 ++-- tests/lean/Avl/Funs.lean | 1 + tests/lean/Betree/Funs.lean | 4 ++++ tests/lean/Bst/Funs.lean | 1 + tests/lean/Hashmap/Funs.lean | 1 + tests/lean/Loops.lean | 8 ++++++-- tests/lean/MiniTree.lean | 1 + tests/lean/RenameAttribute.lean | 1 + tests/lean/Tutorial/Tutorial.lean | 4 ++++ 10 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/pure/PureMicroPasses.ml b/src/pure/PureMicroPasses.ml index 55957f6e..2dd09725 100644 --- a/src/pure/PureMicroPasses.ml +++ b/src/pure/PureMicroPasses.ml @@ -3344,12 +3344,7 @@ let compute_reducible (_ctx : ctx) (transl : pure_fun_translation list) : match trans.f.body with | None -> trans | Some body -> ( - (* Check if the body is exactly a call to a loop function. - Note that we check that the arguments are exactly the input - variables - otherwise we may not want the call to be reducible; - for instance when using the [progress] tactic we might want to - use a more specialized specification theorem. *) - let app, args = destruct_apps body.body in + let app, _ = destruct_apps body.body in match app.e with | Qualif { @@ -3357,20 +3352,10 @@ let compute_reducible (_ctx : ctx) (transl : pure_fun_translation list) : generics = _; } when fid = FRegular trans.f.def_id -> - if - List.length body.inputs = List.length args - && List.for_all - (fun ((var, arg) : var * texpression) -> - match arg.e with - | Var var_id -> var_id = var.id - | _ -> false) - (List.combine body.inputs args) - then - let f = - { trans.f with backend_attributes = { reducible = true } } - in - { trans with f } - else trans + let f = + { trans.f with backend_attributes = { reducible = true } } + in + { trans with f } | _ -> trans) in List.map update_one transl diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 9d965378..57500003 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -375,8 +375,8 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 := /- [arrays::sum]: Source: 'tests/src/arrays.rs', lines 270:0-278:1 -/ -def sum (s : Slice U32) : Result U32 := - sum_loop s 0#u32 0#usize +@[reducible] def sum (s : Slice U32) : Result U32 := + sum_loop s 0#u32 0#usize /- [arrays::sum2]: loop 0: Source: 'tests/src/arrays.rs', lines 284:4-287:5 -/ diff --git a/tests/lean/Avl/Funs.lean b/tests/lean/Avl/Funs.lean index e845aa28..1c151737 100644 --- a/tests/lean/Avl/Funs.lean +++ b/tests/lean/Avl/Funs.lean @@ -221,6 +221,7 @@ divergent def Tree.find_loop /- [avl::{avl::Tree}#3::find]: Source: 'src/avl.rs', lines 342:4-354:5 -/ +@[reducible] def Tree.find {T : Type} (OrdInst : Ord T) (self : Tree T) (value : T) : Result Bool := Tree.find_loop OrdInst value self.root diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 05f05602..07e6a08f 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -94,6 +94,7 @@ divergent def betree.List.len_loop /- [betree::betree::{betree::betree::List}#1::len]: Source: 'src/betree.rs', lines 276:4-284:5 -/ +@[reducible] def betree.List.len {T : Type} (self : betree.List T) : Result U64 := betree.List.len_loop self 0#u64 @@ -110,6 +111,7 @@ divergent def betree.List.reverse_loop /- [betree::betree::{betree::betree::List}#1::reverse]: Source: 'src/betree.rs', lines 304:4-312:5 -/ +@[reducible] def betree.List.reverse {T : Type} (self : betree.List T) : Result (betree.List T) := betree.List.reverse_loop self betree.List.Nil @@ -134,6 +136,7 @@ divergent def betree.List.split_at_loop /- [betree::betree::{betree::betree::List}#1::split_at]: Source: 'src/betree.rs', lines 287:4-302:5 -/ +@[reducible] def betree.List.split_at {T : Type} (self : betree.List T) (n : U64) : Result ((betree.List T) × (betree.List T)) @@ -197,6 +200,7 @@ divergent def betree.ListPairU64T.partition_at_pivot_loop /- [betree::betree::{betree::betree::List<(u64, T)>}#2::partition_at_pivot]: Source: 'src/betree.rs', lines 355:4-370:5 -/ +@[reducible] def betree.ListPairU64T.partition_at_pivot {T : Type} (self : betree.List (U64 × T)) (pivot : U64) : Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) diff --git a/tests/lean/Bst/Funs.lean b/tests/lean/Bst/Funs.lean index d7530285..ddd05e8a 100644 --- a/tests/lean/Bst/Funs.lean +++ b/tests/lean/Bst/Funs.lean @@ -32,6 +32,7 @@ divergent def TreeSet.find_loop /- [bst::{bst::TreeSet}::find]: Source: 'src/bst.rs', lines 32:4-44:5 -/ +@[reducible] def TreeSet.find {T : Type} (OrdInst : Ord T) (self : TreeSet T) (value : T) : Result Bool := TreeSet.find_loop OrdInst value self.root diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index a5e82abe..d1147a69 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -201,6 +201,7 @@ divergent def HashMap.move_elements_loop /- [hashmap::{hashmap::HashMap}::move_elements]: Source: 'tests/src/hashmap.rs', lines 185:4-195:5 -/ +@[reducible] def HashMap.move_elements {T : Type} (ntable : HashMap T) (slots : alloc.vec.Vec (AList T)) : Result ((HashMap T) × (alloc.vec.Vec (AList T))) diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 378a8c27..5955eb67 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -20,8 +20,8 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := /- [loops::sum]: Source: 'tests/src/loops.rs', lines 8:0-18:1 -/ -def sum (max : U32) : Result U32 := - sum_loop max 0#u32 0#u32 +@[reducible] def sum (max : U32) : Result U32 := + sum_loop max 0#u32 0#u32 /- [loops::sum_with_mut_borrows]: loop 0: Source: 'tests/src/loops.rs', lines 26:4-31:5 -/ @@ -37,6 +37,7 @@ divergent def sum_with_mut_borrows_loop /- [loops::sum_with_mut_borrows]: Source: 'tests/src/loops.rs', lines 23:0-35:1 -/ +@[reducible] def sum_with_mut_borrows (max : U32) : Result U32 := sum_with_mut_borrows_loop max 0#u32 0#u32 @@ -54,6 +55,7 @@ divergent def sum_with_shared_borrows_loop /- [loops::sum_with_shared_borrows]: Source: 'tests/src/loops.rs', lines 38:0-52:1 -/ +@[reducible] def sum_with_shared_borrows (max : U32) : Result U32 := sum_with_shared_borrows_loop max 0#u32 0#u32 @@ -72,6 +74,7 @@ divergent def sum_array_loop /- [loops::sum_array]: Source: 'tests/src/loops.rs', lines 54:0-62:1 -/ +@[reducible] def sum_array {N : Usize} (a : Array U32 N) : Result U32 := sum_array_loop a 0#usize 0#u32 @@ -93,6 +96,7 @@ divergent def clear_loop /- [loops::clear]: Source: 'tests/src/loops.rs', lines 66:0-72:1 -/ +@[reducible] def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := clear_loop v 0#usize diff --git a/tests/lean/MiniTree.lean b/tests/lean/MiniTree.lean index 58b1eaac..afc7e495 100644 --- a/tests/lean/MiniTree.lean +++ b/tests/lean/MiniTree.lean @@ -33,6 +33,7 @@ divergent def Tree.explore_loop (current_tree : Option Node) : Result Unit := /- [mini_tree::{mini_tree::Tree}::explore]: Source: 'tests/src/mini_tree.rs', lines 14:4-20:5 -/ +@[reducible] def Tree.explore (self : Tree) : Result Unit := Tree.explore_loop self.root diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean index 17f62b89..e60369f6 100644 --- a/tests/lean/RenameAttribute.lean +++ b/tests/lean/RenameAttribute.lean @@ -88,6 +88,7 @@ divergent def No_borrows_sum_loop /- [rename_attribute::sum]: Source: 'tests/src/rename_attribute.rs', lines 65:0-75:1 -/ +@[reducible] def No_borrows_sum (max : U32) : Result U32 := No_borrows_sum_loop max 0#u32 0#u32 diff --git a/tests/lean/Tutorial/Tutorial.lean b/tests/lean/Tutorial/Tutorial.lean index 2b55e49e..fcb70745 100644 --- a/tests/lean/Tutorial/Tutorial.lean +++ b/tests/lean/Tutorial/Tutorial.lean @@ -218,6 +218,7 @@ divergent def reverse_loop /- [tutorial::reverse]: Source: 'src/lib.rs', lines 146:0-154:1 -/ +@[reducible] def reverse {T : Type} (l : CList T) : Result (CList T) := reverse_loop l CList.CNil @@ -239,6 +240,7 @@ divergent def zero_loop /- [tutorial::zero]: Source: 'src/lib.rs', lines 162:0-168:1 -/ +@[reducible] def zero (x : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := zero_loop x 0#usize @@ -265,6 +267,7 @@ divergent def add_no_overflow_loop /- [tutorial::add_no_overflow]: Source: 'src/lib.rs', lines 175:0-181:1 -/ +@[reducible] def add_no_overflow (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) @@ -302,6 +305,7 @@ divergent def add_with_carry_loop /- [tutorial::add_with_carry]: Source: 'src/lib.rs', lines 186:0-199:1 -/ +@[reducible] def add_with_carry (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) : Result (U8 × (alloc.vec.Vec U32))