From e010c10fb9a1e2d88b52a4f6b4a0865448276013 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jul 2023 15:58:38 +0200 Subject: Make the `by inlit` implicit --- tests/lean/Loops/Funs.lean | 140 ++++++++++++++++++++++----------------------- 1 file changed, 67 insertions(+), 73 deletions(-) (limited to 'tests/lean/Loops/Funs.lean') diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean index 8cac7ac0..f7e6603d 100644 --- a/tests/lean/Loops/Funs.lean +++ b/tests/lean/Loops/Funs.lean @@ -8,16 +8,15 @@ namespace loops /- [loops::sum]: loop 0: forward function -/ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max - then - do - let s0 ← s + i - let i0 ← i + (U32.ofInt 1 (by intlit)) - sum_loop max i0 s0 - else s * (U32.ofInt 2 (by intlit)) + then do + let s0 ← s + i + let i0 ← i + (U32.ofInt 1) + sum_loop max i0 s0 + else s * (U32.ofInt 2) /- [loops::sum]: forward function -/ def sum (max : U32) : Result U32 := - sum_loop max (U32.ofInt 0 (by intlit)) (U32.ofInt 0 (by intlit)) + sum_loop max (U32.ofInt 0) (U32.ofInt 0) /- [loops::sum_with_mut_borrows]: loop 0: forward function -/ divergent def sum_with_mut_borrows_loop @@ -26,14 +25,13 @@ divergent def sum_with_mut_borrows_loop then do let ms0 ← ms + mi - let mi0 ← mi + (U32.ofInt 1 (by intlit)) + let mi0 ← mi + (U32.ofInt 1) sum_with_mut_borrows_loop max mi0 ms0 - else ms * (U32.ofInt 2 (by intlit)) + else ms * (U32.ofInt 2) /- [loops::sum_with_mut_borrows]: forward function -/ def sum_with_mut_borrows (max : U32) : Result U32 := - sum_with_mut_borrows_loop max (U32.ofInt 0 (by intlit)) - (U32.ofInt 0 (by intlit)) + sum_with_mut_borrows_loop max (U32.ofInt 0) (U32.ofInt 0) /- [loops::sum_with_shared_borrows]: loop 0: forward function -/ divergent def sum_with_shared_borrows_loop @@ -41,15 +39,14 @@ divergent def sum_with_shared_borrows_loop if i < max then do - let i0 ← i + (U32.ofInt 1 (by intlit)) + let i0 ← i + (U32.ofInt 1) let s0 ← s + i0 sum_with_shared_borrows_loop max i0 s0 - else s * (U32.ofInt 2 (by intlit)) + else s * (U32.ofInt 2) /- [loops::sum_with_shared_borrows]: forward function -/ def sum_with_shared_borrows (max : U32) : Result U32 := - sum_with_shared_borrows_loop max (U32.ofInt 0 (by intlit)) - (U32.ofInt 0 (by intlit)) + sum_with_shared_borrows_loop max (U32.ofInt 0) (U32.ofInt 0) /- [loops::clear]: loop 0: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ @@ -58,15 +55,15 @@ divergent def clear_loop (v : Vec U32) (i : Usize) : Result (Vec U32) := if i < i0 then do - let i1 ← i + (Usize.ofInt 1 (by intlit)) - let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0 (by intlit)) + let i1 ← i + (Usize.ofInt 1) + let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0) clear_loop v0 i1 else Result.ret v /- [loops::clear]: merged forward/backward function (there is a single backward function, and the forward function returns ()) -/ def clear (v : Vec U32) : Result (Vec U32) := - clear_loop v (Usize.ofInt 0 (by intlit)) + clear_loop v (Usize.ofInt 0) /- [loops::list_mem]: loop 0: forward function -/ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := @@ -85,12 +82,11 @@ divergent def list_nth_mut_loop_loop (T : Type) (ls : List T) (i : U32) : Result T := match ls with | List.Cons x tl => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret x - else - do - let i0 ← i - (U32.ofInt 1 (by intlit)) - list_nth_mut_loop_loop T tl i0 + else do + let i0 ← i - (U32.ofInt 1) + list_nth_mut_loop_loop T tl i0 | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop]: forward function -/ @@ -102,11 +98,11 @@ divergent def list_nth_mut_loop_loop_back (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := match ls with | List.Cons x tl => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 Result.ret (List.Cons x tl0) | List.Nil => Result.fail Error.panic @@ -121,12 +117,11 @@ divergent def list_nth_shared_loop_loop (T : Type) (ls : List T) (i : U32) : Result T := match ls with | List.Cons x tl => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret x - else - do - let i0 ← i - (U32.ofInt 1 (by intlit)) - list_nth_shared_loop_loop T tl i0 + else do + let i0 ← i - (U32.ofInt 1) + list_nth_shared_loop_loop T tl i0 | List.Nil => Result.fail Error.panic /- [loops::list_nth_shared_loop]: forward function -/ @@ -144,7 +139,7 @@ divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize := /- [loops::get_elem_mut]: forward function -/ def get_elem_mut (slots : Vec (List Usize)) (x : Usize) : Result Usize := do - let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit)) + let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0) get_elem_mut_loop x l /- [loops::get_elem_mut]: loop 0: backward function 0 -/ @@ -166,9 +161,9 @@ def get_elem_mut_back Result (Vec (List Usize)) := do - let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit)) + let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0) let l0 ← get_elem_mut_loop_back x l ret0 - Vec.index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0 + Vec.index_mut_back (List Usize) slots (Usize.ofInt 0) l0 /- [loops::get_elem_shared]: loop 0: forward function -/ divergent def get_elem_shared_loop @@ -182,7 +177,7 @@ divergent def get_elem_shared_loop /- [loops::get_elem_shared]: forward function -/ def get_elem_shared (slots : Vec (List Usize)) (x : Usize) : Result Usize := do - let l ← Vec.index (List Usize) slots (Usize.ofInt 0 (by intlit)) + let l ← Vec.index (List Usize) slots (Usize.ofInt 0) get_elem_shared_loop x l /- [loops::id_mut]: forward function -/ @@ -202,12 +197,11 @@ divergent def list_nth_mut_loop_with_id_loop (T : Type) (i : U32) (ls : List T) : Result T := match ls with | List.Cons x tl => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret x - else - do - let i0 ← i - (U32.ofInt 1 (by intlit)) - list_nth_mut_loop_with_id_loop T i0 tl + else do + let i0 ← i - (U32.ofInt 1) + list_nth_mut_loop_with_id_loop T i0 tl | List.Nil => Result.fail Error.panic /- [loops::list_nth_mut_loop_with_id]: forward function -/ @@ -221,11 +215,11 @@ divergent def list_nth_mut_loop_with_id_loop_back (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) := match ls with | List.Cons x tl => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 Result.ret (List.Cons x tl0) | List.Nil => Result.fail Error.panic @@ -243,11 +237,11 @@ divergent def list_nth_shared_loop_with_id_loop (T : Type) (i : U32) (ls : List T) : Result T := match ls with | List.Cons x tl => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret x else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_shared_loop_with_id_loop T i0 tl | List.Nil => Result.fail Error.panic @@ -265,11 +259,11 @@ divergent def list_nth_mut_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_mut_loop_pair_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -288,11 +282,11 @@ divergent def list_nth_mut_loop_pair_loop_back'a | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl0) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 Result.ret (List.Cons x0 tl00) | List.Nil => Result.fail Error.panic @@ -314,11 +308,11 @@ divergent def list_nth_mut_loop_pair_loop_back'b | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 Result.ret (List.Cons x1 tl10) | List.Nil => Result.fail Error.panic @@ -338,11 +332,11 @@ divergent def list_nth_shared_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_shared_loop_pair_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -359,11 +353,11 @@ divergent def list_nth_mut_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -382,12 +376,12 @@ divergent def list_nth_mut_loop_pair_merge_loop_back | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then let (t, t0) := ret0 Result.ret (List.Cons t tl0, List.Cons t0 tl1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let (tl00, tl10) ← list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) @@ -408,11 +402,11 @@ divergent def list_nth_shared_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -429,11 +423,11 @@ divergent def list_nth_mut_shared_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -452,11 +446,11 @@ divergent def list_nth_mut_shared_loop_pair_loop_back | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl0) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl00 ← list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 Result.ret (List.Cons x0 tl00) @@ -477,11 +471,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -500,11 +494,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl0) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl00 ← list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 Result.ret (List.Cons x0 tl00) @@ -525,11 +519,11 @@ divergent def list_nth_shared_mut_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -548,11 +542,11 @@ divergent def list_nth_shared_mut_loop_pair_loop_back | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl10 ← list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 Result.ret (List.Cons x1 tl10) @@ -573,11 +567,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (x0, x1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0 | List.Nil => Result.fail Error.panic | List.Nil => Result.fail Error.panic @@ -596,11 +590,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = (U32.ofInt 0 (by intlit)) + if i = (U32.ofInt 0) then Result.ret (List.Cons ret0 tl1) else do - let i0 ← i - (U32.ofInt 1 (by intlit)) + let i0 ← i - (U32.ofInt 1) let tl10 ← list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 Result.ret (List.Cons x1 tl10) -- cgit v1.2.3