diff options
Diffstat (limited to 'tests/lean')
| -rw-r--r-- | tests/lean/Array.lean | 503 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 1158 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/FunsExternal_Template.lean | 10 | ||||
| -rw-r--r-- | tests/lean/Bitwise.lean | 18 | ||||
| -rw-r--r-- | tests/lean/Constants.lean | 22 | ||||
| -rw-r--r-- | tests/lean/External/Funs.lean | 89 | ||||
| -rw-r--r-- | tests/lean/External/FunsExternal_Template.lean | 19 | ||||
| -rw-r--r-- | tests/lean/Hashmap/Funs.lean | 582 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/Funs.lean | 603 | ||||
| -rw-r--r-- | tests/lean/HashmapMain/FunsExternal_Template.lean | 4 | ||||
| -rw-r--r-- | tests/lean/Loops.lean | 661 | ||||
| -rw-r--r-- | tests/lean/Paper.lean | 131 | ||||
| -rw-r--r-- | tests/lean/PoloniusList.lean | 35 | ||||
| -rw-r--r-- | tests/lean/Traits.lean | 161 |
14 files changed, 1635 insertions, 2361 deletions
diff --git a/tests/lean/Array.lean b/tests/lean/Array.lean index 25dad3cf..20f3425e 100644 --- a/tests/lean/Array.lean +++ b/tests/lean/Array.lean @@ -11,99 +11,94 @@ inductive AB := | A : AB | B : AB -/- [array::incr]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [array::incr]: Source: 'src/array.rs', lines 8:0-8:24 -/ def incr (x : U32) : Result U32 := x + 1#u32 -/- [array::array_to_shared_slice_]: forward function +/- [array::array_to_shared_slice_]: Source: 'src/array.rs', lines 16:0-16:53 -/ def array_to_shared_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) := Array.to_slice T 32#usize s -/- [array::array_to_mut_slice_]: forward function +/- [array::array_to_mut_slice_]: Source: 'src/array.rs', lines 21:0-21:58 -/ -def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) := - Array.to_slice T 32#usize s - -/- [array::array_to_mut_slice_]: backward function 0 - Source: 'src/array.rs', lines 21:0-21:58 -/ -def array_to_mut_slice__back - (T : Type) (s : Array T 32#usize) (ret : Slice T) : - Result (Array T 32#usize) +def array_to_mut_slice_ + (T : Type) (s : Array T 32#usize) : + Result ((Slice T) × (Slice T → Result (Array T 32#usize))) := - Array.from_slice T 32#usize s ret + do + let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s + let back := fun ret => to_slice_mut_back ret + Result.ret (s1, back) -/- [array::array_len]: forward function +/- [array::array_len]: Source: 'src/array.rs', lines 25:0-25:40 -/ def array_len (T : Type) (s : Array T 32#usize) : Result Usize := do - let s0 ← Array.to_slice T 32#usize s - let i := Slice.len T s0 - Result.ret i + let s1 ← Array.to_slice T 32#usize s + let i := Slice.len T s1 + Result.ret i -/- [array::shared_array_len]: forward function +/- [array::shared_array_len]: Source: 'src/array.rs', lines 29:0-29:48 -/ def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := do - let s0 ← Array.to_slice T 32#usize s - let i := Slice.len T s0 - Result.ret i + let s1 ← Array.to_slice T 32#usize s + let i := Slice.len T s1 + Result.ret i -/- [array::shared_slice_len]: forward function +/- [array::shared_slice_len]: Source: 'src/array.rs', lines 33:0-33:44 -/ def shared_slice_len (T : Type) (s : Slice T) : Result Usize := let i := Slice.len T s Result.ret i -/- [array::index_array_shared]: forward function +/- [array::index_array_shared]: Source: 'src/array.rs', lines 37:0-37:57 -/ def index_array_shared (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := Array.index_usize T 32#usize s i -/- [array::index_array_u32]: forward function +/- [array::index_array_u32]: Source: 'src/array.rs', lines 44:0-44:53 -/ def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 := Array.index_usize U32 32#usize s i -/- [array::index_array_copy]: forward function +/- [array::index_array_copy]: Source: 'src/array.rs', lines 48:0-48:45 -/ def index_array_copy (x : Array U32 32#usize) : Result U32 := Array.index_usize U32 32#usize x 0#usize -/- [array::index_mut_array]: forward function +/- [array::index_mut_array]: Source: 'src/array.rs', lines 52:0-52:62 -/ -def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := - Array.index_usize T 32#usize s i - -/- [array::index_mut_array]: backward function 0 - Source: 'src/array.rs', lines 52:0-52:62 -/ -def index_mut_array_back - (T : Type) (s : Array T 32#usize) (i : Usize) (ret : T) : - Result (Array T 32#usize) +def index_mut_array + (T : Type) (s : Array T 32#usize) (i : Usize) : + Result (T × (T → Result (Array T 32#usize))) := - Array.update_usize T 32#usize s i ret + do + let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i + let back := fun ret => index_mut_back ret + Result.ret (t, back) -/- [array::index_slice]: forward function +/- [array::index_slice]: Source: 'src/array.rs', lines 56:0-56:46 -/ def index_slice (T : Type) (s : Slice T) (i : Usize) : Result T := Slice.index_usize T s i -/- [array::index_mut_slice]: forward function +/- [array::index_mut_slice]: Source: 'src/array.rs', lines 60:0-60:58 -/ -def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result T := - Slice.index_usize T s i - -/- [array::index_mut_slice]: backward function 0 - Source: 'src/array.rs', lines 60:0-60:58 -/ -def index_mut_slice_back - (T : Type) (s : Slice T) (i : Usize) (ret : T) : Result (Slice T) := - Slice.update_usize T s i ret +def index_mut_slice + (T : Type) (s : Slice T) (i : Usize) : + Result (T × (T → Result (Slice T))) + := + do + let (t, index_mut_back) ← Slice.index_mut_usize T s i + let back := fun ret => index_mut_back ret + Result.ret (t, back) -/- [array::slice_subslice_shared_]: forward function +/- [array::slice_subslice_shared_]: Source: 'src/array.rs', lines 64:0-64:70 -/ def slice_subslice_shared_ (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) := @@ -111,41 +106,37 @@ def slice_subslice_shared_ (core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x { start := y, end_ := z } -/- [array::slice_subslice_mut_]: forward function +/- [array::slice_subslice_mut_]: Source: 'src/array.rs', lines 68:0-68:75 -/ def slice_subslice_mut_ - (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) := - core.slice.index.Slice.index_mut U32 (core.ops.range.Range Usize) - (core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x - { start := y, end_ := z } - -/- [array::slice_subslice_mut_]: backward function 0 - Source: 'src/array.rs', lines 68:0-68:75 -/ -def slice_subslice_mut__back - (x : Slice U32) (y : Usize) (z : Usize) (ret : Slice U32) : - Result (Slice U32) + (x : Slice U32) (y : Usize) (z : Usize) : + Result ((Slice U32) × (Slice U32 → Result (Slice U32))) := - core.slice.index.Slice.index_mut_back U32 (core.ops.range.Range Usize) - (core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x - { start := y, end_ := z } ret - -/- [array::array_to_slice_shared_]: forward function + do + let (s, index_mut_back) ← + core.slice.index.Slice.index_mut U32 (core.ops.range.Range Usize) + (core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x + { start := y, end_ := z } + let back := fun ret => index_mut_back ret + Result.ret (s, back) + +/- [array::array_to_slice_shared_]: Source: 'src/array.rs', lines 72:0-72:54 -/ def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) := Array.to_slice U32 32#usize x -/- [array::array_to_slice_mut_]: forward function +/- [array::array_to_slice_mut_]: Source: 'src/array.rs', lines 76:0-76:59 -/ -def array_to_slice_mut_ (x : Array U32 32#usize) : Result (Slice U32) := - Array.to_slice U32 32#usize x - -/- [array::array_to_slice_mut_]: backward function 0 - Source: 'src/array.rs', lines 76:0-76:59 -/ -def array_to_slice_mut__back - (x : Array U32 32#usize) (ret : Slice U32) : Result (Array U32 32#usize) := - Array.from_slice U32 32#usize x ret +def array_to_slice_mut_ + (x : Array U32 32#usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) + := + do + let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x + let back := fun ret => to_slice_mut_back ret + Result.ret (s, back) -/- [array::array_subslice_shared_]: forward function +/- [array::array_subslice_shared_]: Source: 'src/array.rs', lines 80:0-80:74 -/ def array_subslice_shared_ (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := @@ -154,311 +145,295 @@ def array_subslice_shared_ (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } -/- [array::array_subslice_mut_]: forward function +/- [array::array_subslice_mut_]: Source: 'src/array.rs', lines 84:0-84:79 -/ def array_subslice_mut_ - (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize - (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) - (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x - { start := y, end_ := z } - -/- [array::array_subslice_mut_]: backward function 0 - Source: 'src/array.rs', lines 84:0-84:79 -/ -def array_subslice_mut__back - (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret : Slice U32) : - Result (Array U32 32#usize) + (x : Array U32 32#usize) (y : Usize) (z : Usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) := - core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 32#usize - (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) - (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x - { start := y, end_ := z } ret - -/- [array::index_slice_0]: forward function + do + let (s, index_mut_back) ← + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize + (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) + (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x + { start := y, end_ := z } + let back := fun ret => index_mut_back ret + Result.ret (s, back) + +/- [array::index_slice_0]: Source: 'src/array.rs', lines 88:0-88:38 -/ def index_slice_0 (T : Type) (s : Slice T) : Result T := Slice.index_usize T s 0#usize -/- [array::index_array_0]: forward function +/- [array::index_array_0]: Source: 'src/array.rs', lines 92:0-92:42 -/ def index_array_0 (T : Type) (s : Array T 32#usize) : Result T := Array.index_usize T 32#usize s 0#usize -/- [array::index_index_array]: forward function +/- [array::index_index_array]: Source: 'src/array.rs', lines 103:0-103:71 -/ def index_index_array (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : Result U32 := do - let a ← Array.index_usize (Array U32 32#usize) 32#usize s i - Array.index_usize U32 32#usize a j + let a ← Array.index_usize (Array U32 32#usize) 32#usize s i + Array.index_usize U32 32#usize a j -/- [array::update_update_array]: forward function +/- [array::update_update_array]: Source: 'src/array.rs', lines 114:0-114:70 -/ def update_update_array (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : Result Unit := do - let a ← Array.index_usize (Array U32 32#usize) 32#usize s i - let a0 ← Array.update_usize U32 32#usize a j 0#u32 - let _ ← Array.update_usize (Array U32 32#usize) 32#usize s i a0 - Result.ret () + let (a, index_mut_back) ← + Array.index_mut_usize (Array U32 32#usize) 32#usize s i + let (_, index_mut_back1) ← Array.index_mut_usize U32 32#usize a j + let a1 ← index_mut_back1 0#u32 + let _ ← index_mut_back a1 + Result.ret () -/- [array::array_local_deep_copy]: forward function +/- [array::array_local_deep_copy]: Source: 'src/array.rs', lines 118:0-118:43 -/ def array_local_deep_copy (x : Array U32 32#usize) : Result Unit := Result.ret () -/- [array::take_array]: forward function +/- [array::take_array]: Source: 'src/array.rs', lines 122:0-122:30 -/ def take_array (a : Array U32 2#usize) : Result Unit := Result.ret () -/- [array::take_array_borrow]: forward function +/- [array::take_array_borrow]: Source: 'src/array.rs', lines 123:0-123:38 -/ def take_array_borrow (a : Array U32 2#usize) : Result Unit := Result.ret () -/- [array::take_slice]: forward function +/- [array::take_slice]: Source: 'src/array.rs', lines 124:0-124:28 -/ def take_slice (s : Slice U32) : Result Unit := Result.ret () -/- [array::take_mut_slice]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [array::take_mut_slice]: Source: 'src/array.rs', lines 125:0-125:36 -/ def take_mut_slice (s : Slice U32) : Result (Slice U32) := Result.ret s -/- [array::const_array]: forward function +/- [array::const_array]: Source: 'src/array.rs', lines 127:0-127:32 -/ def const_array : Result (Array U32 2#usize) := Result.ret (Array.make U32 2#usize [ 0#u32, 0#u32 ]) -/- [array::const_slice]: forward function +/- [array::const_slice]: Source: 'src/array.rs', lines 131:0-131:20 -/ def const_slice : Result Unit := do - let _ ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - Result.ret () + let _ ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Result.ret () -/- [array::take_all]: forward function +/- [array::take_all]: Source: 'src/array.rs', lines 141:0-141:17 -/ def take_all : Result Unit := do - let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let _ ← take_slice s - let s0 ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let s1 ← take_mut_slice s0 - let _ ← - Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 - Result.ret () - -/- [array::index_array]: forward function + let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_slice s + let (s1, to_slice_mut_back) ← + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s2 ← take_mut_slice s1 + let _ ← to_slice_mut_back s2 + Result.ret () + +/- [array::index_array]: Source: 'src/array.rs', lines 155:0-155:38 -/ def index_array (x : Array U32 2#usize) : Result U32 := Array.index_usize U32 2#usize x 0#usize -/- [array::index_array_borrow]: forward function +/- [array::index_array_borrow]: Source: 'src/array.rs', lines 158:0-158:46 -/ def index_array_borrow (x : Array U32 2#usize) : Result U32 := Array.index_usize U32 2#usize x 0#usize -/- [array::index_slice_u32_0]: forward function +/- [array::index_slice_u32_0]: Source: 'src/array.rs', lines 162:0-162:42 -/ def index_slice_u32_0 (x : Slice U32) : Result U32 := Slice.index_usize U32 x 0#usize -/- [array::index_mut_slice_u32_0]: forward function +/- [array::index_mut_slice_u32_0]: Source: 'src/array.rs', lines 166:0-166:50 -/ -def index_mut_slice_u32_0 (x : Slice U32) : Result U32 := - Slice.index_usize U32 x 0#usize - -/- [array::index_mut_slice_u32_0]: backward function 0 - Source: 'src/array.rs', lines 166:0-166:50 -/ -def index_mut_slice_u32_0_back (x : Slice U32) : Result (Slice U32) := +def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) := do - let _ ← Slice.index_usize U32 x 0#usize - Result.ret x + let i ← Slice.index_usize U32 x 0#usize + Result.ret (i, x) -/- [array::index_all]: forward function +/- [array::index_all]: Source: 'src/array.rs', lines 170:0-170:25 -/ def index_all : Result U32 := do - let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let i0 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let i1 ← i + i0 - let i2 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let i3 ← i1 + i2 - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let i4 ← index_slice_u32_0 s - let i5 ← i3 + i4 - let s0 ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let i6 ← index_mut_slice_u32_0 s0 - let i7 ← i5 + i6 - let s1 ← index_mut_slice_u32_0_back s0 - let _ ← - Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 - Result.ret i7 - -/- [array::update_array]: forward function + let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i1 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i2 ← i + i1 + let i3 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i4 ← i2 + i3 + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i5 ← index_slice_u32_0 s + let i6 ← i4 + i5 + let (s1, to_slice_mut_back) ← + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let (i7, s2) ← index_mut_slice_u32_0 s1 + let i8 ← i6 + i7 + let _ ← to_slice_mut_back s2 + Result.ret i8 + +/- [array::update_array]: Source: 'src/array.rs', lines 184:0-184:36 -/ def update_array (x : Array U32 2#usize) : Result Unit := do - let _ ← Array.update_usize U32 2#usize x 0#usize 1#u32 - Result.ret () + let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize + let _ ← index_mut_back 1#u32 + Result.ret () -/- [array::update_array_mut_borrow]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [array::update_array_mut_borrow]: Source: 'src/array.rs', lines 187:0-187:48 -/ def update_array_mut_borrow (x : Array U32 2#usize) : Result (Array U32 2#usize) := - Array.update_usize U32 2#usize x 0#usize 1#u32 + do + let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize + index_mut_back 1#u32 -/- [array::update_mut_slice]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [array::update_mut_slice]: Source: 'src/array.rs', lines 190:0-190:38 -/ def update_mut_slice (x : Slice U32) : Result (Slice U32) := - Slice.update_usize U32 x 0#usize 1#u32 + do + let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0#usize + index_mut_back 1#u32 -/- [array::update_all]: forward function +/- [array::update_all]: Source: 'src/array.rs', lines 194:0-194:19 -/ def update_all : Result Unit := do - let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let s ← Array.to_slice U32 2#usize x - let s0 ← update_mut_slice s - let _ ← Array.from_slice U32 2#usize x s0 - Result.ret () - -/- [array::range_all]: forward function + let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let a ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize a + let s1 ← update_mut_slice s + let _ ← to_slice_mut_back s1 + Result.ret () + +/- [array::range_all]: Source: 'src/array.rs', lines 205:0-205:18 -/ def range_all : Result Unit := do - let s ← - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize - (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) - (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) - (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) - { start := 1#usize, end_ := 3#usize } - let s0 ← update_mut_slice s - let _ ← - core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 4#usize - (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) - (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) - (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) - { start := 1#usize, end_ := 3#usize } s0 - Result.ret () - -/- [array::deref_array_borrow]: forward function + let (s, index_mut_back) ← + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize + (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) + (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) + (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) + { start := 1#usize, end_ := 3#usize } + let s1 ← update_mut_slice s + let _ ← index_mut_back s1 + Result.ret () + +/- [array::deref_array_borrow]: Source: 'src/array.rs', lines 214:0-214:46 -/ def deref_array_borrow (x : Array U32 2#usize) : Result U32 := Array.index_usize U32 2#usize x 0#usize -/- [array::deref_array_mut_borrow]: forward function - Source: 'src/array.rs', lines 219:0-219:54 -/ -def deref_array_mut_borrow (x : Array U32 2#usize) : Result U32 := - Array.index_usize U32 2#usize x 0#usize - -/- [array::deref_array_mut_borrow]: backward function 0 +/- [array::deref_array_mut_borrow]: Source: 'src/array.rs', lines 219:0-219:54 -/ -def deref_array_mut_borrow_back - (x : Array U32 2#usize) : Result (Array U32 2#usize) := +def deref_array_mut_borrow + (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) := do - let _ ← Array.index_usize U32 2#usize x 0#usize - Result.ret x + let i ← Array.index_usize U32 2#usize x 0#usize + Result.ret (i, x) -/- [array::take_array_t]: forward function +/- [array::take_array_t]: Source: 'src/array.rs', lines 227:0-227:31 -/ def take_array_t (a : Array AB 2#usize) : Result Unit := Result.ret () -/- [array::non_copyable_array]: forward function +/- [array::non_copyable_array]: Source: 'src/array.rs', lines 229:0-229:27 -/ def non_copyable_array : Result Unit := do - let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) - Result.ret () + let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) + Result.ret () -/- [array::sum]: loop 0: forward function +/- [array::sum]: loop 0: Source: 'src/array.rs', lines 242:0-250:1 -/ -divergent def sum_loop (s : Slice U32) (sum0 : U32) (i : Usize) : Result U32 := - let i0 := Slice.len U32 s - if i < i0 +divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 := + let i1 := Slice.len U32 s + if i < i1 then do - let i1 ← Slice.index_usize U32 s i - let sum1 ← sum0 + i1 - let i2 ← i + 1#usize - sum_loop s sum1 i2 - else Result.ret sum0 + let i2 ← Slice.index_usize U32 s i + let sum3 ← sum1 + i2 + let i3 ← i + 1#usize + sum_loop s sum3 i3 + else Result.ret sum1 -/- [array::sum]: forward function +/- [array::sum]: Source: 'src/array.rs', lines 242:0-242:28 -/ def sum (s : Slice U32) : Result U32 := sum_loop s 0#u32 0#usize -/- [array::sum2]: loop 0: forward function +/- [array::sum2]: loop 0: Source: 'src/array.rs', lines 252:0-261:1 -/ divergent def sum2_loop - (s : Slice U32) (s2 : Slice U32) (sum0 : U32) (i : Usize) : Result U32 := - let i0 := Slice.len U32 s - if i < i0 + (s : Slice U32) (s2 : Slice U32) (sum1 : U32) (i : Usize) : Result U32 := + let i1 := Slice.len U32 s + if i < i1 then do - let i1 ← Slice.index_usize U32 s i - let i2 ← Slice.index_usize U32 s2 i - let i3 ← i1 + i2 - let sum1 ← sum0 + i3 - let i4 ← i + 1#usize - sum2_loop s s2 sum1 i4 - else Result.ret sum0 - -/- [array::sum2]: forward function + let i2 ← Slice.index_usize U32 s i + let i3 ← Slice.index_usize U32 s2 i + let i4 ← i2 + i3 + let sum3 ← sum1 + i4 + let i5 ← i + 1#usize + sum2_loop s s2 sum3 i5 + else Result.ret sum1 + +/- [array::sum2]: Source: 'src/array.rs', lines 252:0-252:41 -/ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := let i := Slice.len U32 s - let i0 := Slice.len U32 s2 - if not (i = i0) + let i1 := Slice.len U32 s2 + if not (i = i1) then Result.fail .panic else sum2_loop s s2 0#u32 0#usize -/- [array::f0]: forward function +/- [array::f0]: Source: 'src/array.rs', lines 263:0-263:11 -/ def f0 : Result Unit := do - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - let s0 ← Slice.update_usize U32 s 0#usize 1#u32 - let _ ← - Array.from_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) s0 - Result.ret () - -/- [array::f1]: forward function + let (s, to_slice_mut_back) ← + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0#usize + let s1 ← index_mut_back 1#u32 + let _ ← to_slice_mut_back s1 + Result.ret () + +/- [array::f1]: Source: 'src/array.rs', lines 268:0-268:11 -/ def f1 : Result Unit := do - let _ ← - Array.update_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - 0#usize 1#u32 - Result.ret () + let (_, index_mut_back) ← + Array.index_mut_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 0#usize + let _ ← index_mut_back 1#u32 + Result.ret () -/- [array::f2]: forward function +/- [array::f2]: Source: 'src/array.rs', lines 273:0-273:17 -/ def f2 (i : U32) : Result Unit := Result.ret () -/- [array::f4]: forward function +/- [array::f4]: Source: 'src/array.rs', lines 282:0-282:54 -/ def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize @@ -466,44 +441,42 @@ def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } -/- [array::f3]: forward function +/- [array::f3]: Source: 'src/array.rs', lines 275:0-275:18 -/ def f3 : Result U32 := do - let i ← - Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - 0#usize - let _ ← f2 i - let b := Array.repeat U32 32#usize 0#u32 - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - let s0 ← f4 b 16#usize 18#usize - sum2 s s0 + let i ← + Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 0#usize + let _ ← f2 i + let b := Array.repeat U32 32#usize 0#u32 + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + let s1 ← f4 b 16#usize 18#usize + sum2 s s1 /- [array::SZ] Source: 'src/array.rs', lines 286:0-286:19 -/ def sz_body : Result Usize := Result.ret 32#usize def sz_c : Usize := eval_global sz_body (by simp) -/- [array::f5]: forward function +/- [array::f5]: Source: 'src/array.rs', lines 289:0-289:31 -/ def f5 (x : Array U32 32#usize) : Result U32 := Array.index_usize U32 32#usize x 0#usize -/- [array::ite]: forward function +/- [array::ite]: Source: 'src/array.rs', lines 294:0-294:12 -/ def ite : Result Unit := do - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let s0 ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let s1 ← index_mut_slice_u32_0_back s0 - let _ ← - Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 - let s2 ← index_mut_slice_u32_0_back s - let _ ← - Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s2 - Result.ret () + let (s, to_slice_mut_back) ← + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let (_, s1) ← index_mut_slice_u32_0 s + let (s2, to_slice_mut_back1) ← + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let (_, s3) ← index_mut_slice_u32_0 s2 + let _ ← to_slice_mut_back1 s3 + let _ ← to_slice_mut_back s1 + Result.ret () end array diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 0d7cb984..4e64d217 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -7,7 +7,7 @@ open Primitives namespace betree_main -/- [betree_main::betree::load_internal_node]: forward function +/- [betree_main::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 -/ def betree.load_internal_node (id : U64) (st : State) : @@ -15,65 +15,53 @@ def betree.load_internal_node := betree_utils.load_internal_node id st -/- [betree_main::betree::store_internal_node]: forward function +/- [betree_main::betree::store_internal_node]: Source: 'src/betree.rs', lines 41:0-41:60 -/ def betree.store_internal_node (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) : Result (State × Unit) := do - let (st0, _) ← betree_utils.store_internal_node id content st - Result.ret (st0, ()) + let (st1, _) ← betree_utils.store_internal_node id content st + Result.ret (st1, ()) -/- [betree_main::betree::load_leaf_node]: forward function +/- [betree_main::betree::load_leaf_node]: Source: 'src/betree.rs', lines 46:0-46:44 -/ def betree.load_leaf_node (id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) := betree_utils.load_leaf_node id st -/- [betree_main::betree::store_leaf_node]: forward function +/- [betree_main::betree::store_leaf_node]: Source: 'src/betree.rs', lines 51:0-51:52 -/ def betree.store_leaf_node (id : U64) (content : betree.List (U64 × U64)) (st : State) : Result (State × Unit) := do - let (st0, _) ← betree_utils.store_leaf_node id content st - Result.ret (st0, ()) + let (st1, _) ← betree_utils.store_leaf_node id content st + Result.ret (st1, ()) -/- [betree_main::betree::fresh_node_id]: forward function +/- [betree_main::betree::fresh_node_id]: Source: 'src/betree.rs', lines 55:0-55:48 -/ -def betree.fresh_node_id (counter : U64) : Result U64 := +def betree.fresh_node_id (counter : U64) : Result (U64 × U64) := do - let _ ← counter + 1#u64 - Result.ret counter + let counter1 ← counter + 1#u64 + Result.ret (counter, counter1) -/- [betree_main::betree::fresh_node_id]: backward function 0 - Source: 'src/betree.rs', lines 55:0-55:48 -/ -def betree.fresh_node_id_back (counter : U64) : Result U64 := - counter + 1#u64 - -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function +/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 -/ def betree.NodeIdCounter.new : Result betree.NodeIdCounter := Result.ret { next_node_id := 0#u64 } -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function +/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 -/ -def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 := +def betree.NodeIdCounter.fresh_id + (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) := do - let _ ← self.next_node_id + 1#u64 - Result.ret self.next_node_id + let i ← self.next_node_id + 1#u64 + Result.ret (self.next_node_id, { next_node_id := i }) -/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 - Source: 'src/betree.rs', lines 210:4-210:36 -/ -def betree.NodeIdCounter.fresh_id_back - (self : betree.NodeIdCounter) : Result betree.NodeIdCounter := - do - let i ← self.next_node_id + 1#u64 - Result.ret { next_node_id := i } - -/- [betree_main::betree::upsert_update]: forward function +/- [betree_main::betree::upsert_update]: Source: 'src/betree.rs', lines 234:0-234:70 -/ def betree.upsert_update (prev : Option U64) (st : betree.UpsertFunState) : Result U64 := @@ -81,30 +69,30 @@ def betree.upsert_update | none => match st with | betree.UpsertFunState.Add v => Result.ret v - | betree.UpsertFunState.Sub i => Result.ret 0#u64 - | some prev0 => + | betree.UpsertFunState.Sub _ => Result.ret 0#u64 + | some prev1 => match st with | betree.UpsertFunState.Add v => do - let margin ← core_u64_max - prev0 - if margin >= v - then prev0 + v - else Result.ret core_u64_max + let margin ← core_u64_max - prev1 + if margin >= v + then prev1 + v + else Result.ret core_u64_max | betree.UpsertFunState.Sub v => - if prev0 >= v - then prev0 - v + if prev1 >= v + then prev1 - v else Result.ret 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function +/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := match self with - | betree.List.Cons t tl => do - let i ← betree.List.len T tl - 1#u64 + i + | betree.List.Cons _ tl => do + let i ← betree.List.len T tl + 1#u64 + i | betree.List.Nil => Result.ret 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function +/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 -/ divergent def betree.List.split_at (T : Type) (self : betree.List T) (n : U64) : @@ -116,56 +104,47 @@ divergent def betree.List.split_at match self with | betree.List.Cons hd tl => do - let i ← n - 1#u64 - let p ← betree.List.split_at T tl i - let (ls0, ls1) := p - let l := ls0 - Result.ret (betree.List.Cons hd l, ls1) + let i ← n - 1#u64 + let p ← betree.List.split_at T tl i + let (ls0, ls1) := p + let l := ls0 + Result.ret (betree.List.Cons hd l, ls1) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299:34 -/ def betree.List.push_front (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := - let tl := core.mem.replace (betree.List T) self betree.List.Nil + let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil let l := tl Result.ret (betree.List.Cons x l) -/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function - Source: 'src/betree.rs', lines 306:4-306:32 -/ -def betree.List.pop_front (T : Type) (self : betree.List T) : Result T := - let ls := core.mem.replace (betree.List T) self betree.List.Nil - match ls with - | betree.List.Cons x tl => Result.ret x - | betree.List.Nil => Result.fail .panic - -/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 +/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: Source: 'src/betree.rs', lines 306:4-306:32 -/ -def betree.List.pop_front_back - (T : Type) (self : betree.List T) : Result (betree.List T) := - let ls := core.mem.replace (betree.List T) self betree.List.Nil +def betree.List.pop_front + (T : Type) (self : betree.List T) : Result (T × (betree.List T)) := + let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil match ls with - | betree.List.Cons x tl => Result.ret tl + | betree.List.Cons x tl => Result.ret (x, tl) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function +/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with - | betree.List.Cons hd l => Result.ret hd + | betree.List.Cons hd _ => Result.ret hd | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function +/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: Source: 'src/betree.rs', lines 327:4-327:44 -/ def betree.ListTupleU64T.head_has_key (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := match self with - | betree.List.Cons hd l => let (i, _) := hd + | betree.List.Cons hd _ => let (i, _) := hd Result.ret (i = key) | betree.List.Nil => Result.ret false -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function +/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: Source: 'src/betree.rs', lines 339:4-339:73 -/ divergent def betree.ListTupleU64T.partition_at_pivot (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : @@ -178,334 +157,191 @@ divergent def betree.ListTupleU64T.partition_at_pivot then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl) else do - let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot - let (ls0, ls1) := p - let l := ls0 - Result.ret (betree.List.Cons (i, t) l, ls1) + let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot + let (ls0, ls1) := p + let l := ls0 + Result.ret (betree.List.Cons (i, t) l, ls1) | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil) -/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function +/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: Source: 'src/betree.rs', lines 359:4-364:17 -/ def betree.Leaf.split (self : betree.Leaf) (content : betree.List (U64 × U64)) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : - Result (State × betree.Internal) + Result (State × (betree.Internal × betree.NodeIdCounter)) := do - let p ← betree.List.split_at (U64 × U64) content params.split_size - let (content0, content1) := p - let p0 ← betree.List.hd (U64 × U64) content1 - let (pivot, _) := p0 - let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt - let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt - let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0 - let (st0, _) ← betree.store_leaf_node id0 content0 st - let (st1, _) ← betree.store_leaf_node id1 content1 st0 - let n := betree.Node.Leaf { id := id0, size := params.split_size } - let n0 := betree.Node.Leaf { id := id1, size := params.split_size } - Result.ret (st1, betree.Internal.mk self.id pivot n n0) - -/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 - Source: 'src/betree.rs', lines 359:4-364:17 -/ -def betree.Leaf.split_back - (self : betree.Leaf) (content : betree.List (U64 × U64)) - (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) : - Result betree.NodeIdCounter - := - do - let p ← betree.List.split_at (U64 × U64) content params.split_size - let (content0, content1) := p - let _ ← betree.List.hd (U64 × U64) content1 - let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt - let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt - let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0 - let (st0, _) ← betree.store_leaf_node id0 content0 st - let _ ← betree.store_leaf_node id1 content1 st0 - betree.NodeIdCounter.fresh_id_back node_id_cnt0 - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function + let p ← betree.List.split_at (U64 × U64) content params.split_size + let (content0, content1) := p + let p1 ← betree.List.hd (U64 × U64) content1 + let (pivot, _) := p1 + let (id0, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id1, nic1) ← betree.NodeIdCounter.fresh_id nic + let (st1, _) ← betree.store_leaf_node id0 content0 st + let (st2, _) ← betree.store_leaf_node id1 content1 st1 + let n := betree.Node.Leaf { id := id0, size := params.split_size } + let n1 := betree.Node.Leaf { id := id1, size := params.split_size } + Result.ret (st2, (betree.Internal.mk self.id pivot n n1, nic1)) + +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: Source: 'src/betree.rs', lines 789:4-792:34 -/ divergent def betree.Node.lookup_first_message_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) := match msgs with | betree.List.Cons x next_msgs => let (i, m) := x if i >= key - then Result.ret (betree.List.Cons (i, m) next_msgs) - else betree.Node.lookup_first_message_for_key key next_msgs - | betree.List.Nil => Result.ret betree.List.Nil - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 - Source: 'src/betree.rs', lines 789:4-792:34 -/ -divergent def betree.Node.lookup_first_message_for_key_back - (key : U64) (msgs : betree.List (U64 × betree.Message)) - (ret : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) - := - match msgs with - | betree.List.Cons x next_msgs => - let (i, m) := x - if i >= key - then Result.ret ret + then + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Cons (i, m) next_msgs, back_'a) else do - let next_msgs0 ← - betree.Node.lookup_first_message_for_key_back key next_msgs ret - Result.ret (betree.List.Cons (i, m) next_msgs0) - | betree.List.Nil => Result.ret ret - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function + let (l, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key next_msgs + let back_'a := + fun ret => + do + let next_msgs1 ← lookup_first_message_for_key_back ret + Result.ret (betree.List.Cons (i, m) next_msgs1) + Result.ret (l, back_'a) + | betree.List.Nil => + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Nil, back_'a) + +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: Source: 'src/betree.rs', lines 636:4-636:80 -/ divergent def betree.Node.lookup_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) := match bindings with | betree.List.Cons hd tl => - let (i, i0) := hd + let (i, i1) := hd if i = key - then Result.ret (some i0) + then Result.ret (some i1) else if i > key then Result.ret none else betree.Node.lookup_in_bindings key tl | betree.List.Nil => Result.ret none -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: Source: 'src/betree.rs', lines 819:4-819:90 -/ divergent def betree.Node.apply_upserts (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) (st : State) : - Result (State × U64) + Result (State × (U64 × (betree.List (U64 × betree.Message)))) := do - let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key - if b - then - do - let msg ← betree.List.pop_front (U64 × betree.Message) msgs - let (_, m) := msg - match m with - | betree.Message.Insert i => Result.fail .panic - | betree.Message.Delete => Result.fail .panic - | betree.Message.Upsert s => - do - let v ← betree.upsert_update prev s - let msgs0 ← - betree.List.pop_front_back (U64 × betree.Message) msgs - betree.Node.apply_upserts msgs0 (some v) key st - else - do - let (st0, v) ← core.option.Option.unwrap U64 prev st - let _ ← - betree.List.push_front (U64 × betree.Message) msgs (key, - betree.Message.Insert v) - Result.ret (st0, v) - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 - Source: 'src/betree.rs', lines 819:4-819:90 -/ -divergent def betree.Node.apply_upserts_back - (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64) - (st : State) : - Result (betree.List (U64 × betree.Message)) - := - do - let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key - if b - then - do - let msg ← betree.List.pop_front (U64 × betree.Message) msgs - let (_, m) := msg - match m with - | betree.Message.Insert i => Result.fail .panic - | betree.Message.Delete => Result.fail .panic - | betree.Message.Upsert s => - do - let v ← betree.upsert_update prev s - let msgs0 ← - betree.List.pop_front_back (U64 × betree.Message) msgs - betree.Node.apply_upserts_back msgs0 (some v) key st - else + let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key + if b + then + do + let (msg, l) ← betree.List.pop_front (U64 × betree.Message) msgs + let (_, m) := msg + match m with + | betree.Message.Insert _ => Result.fail .panic + | betree.Message.Delete => Result.fail .panic + | betree.Message.Upsert s => do - let (_, v) ← core.option.Option.unwrap U64 prev st - betree.List.push_front (U64 × betree.Message) msgs (key, - betree.Message.Insert v) + let v ← betree.upsert_update prev s + betree.Node.apply_upserts l (some v) key st + else + do + let (st1, v) ← core.option.Option.unwrap U64 prev st + let l ← + betree.List.push_front (U64 × betree.Message) msgs (key, + betree.Message.Insert v) + Result.ret (st1, (v, l)) -/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function +/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: Source: 'src/betree.rs', lines 395:4-395:63 -/ mutual divergent def betree.Internal.lookup_in_children (self : betree.Internal) (key : U64) (st : State) : - Result (State × (Option U64)) + Result (State × ((Option U64) × betree.Internal)) := - let ⟨ _, i, n, n0 ⟩ := self - if key < i - then betree.Node.lookup n key st - else betree.Node.lookup n0 key st - -/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 - Source: 'src/betree.rs', lines 395:4-395:63 -/ -divergent def betree.Internal.lookup_in_children_back - (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal := - let ⟨ i, i0, n, n0 ⟩ := self - if key < i0 + let ⟨ i, i1, n, n1 ⟩ := self + if key < i1 then do - let n1 ← betree.Node.lookup_back n key st - Result.ret (betree.Internal.mk i i0 n1 n0) + let (st1, (o, n2)) ← betree.Node.lookup n key st + Result.ret (st1, (o, betree.Internal.mk i i1 n2 n1)) else do - let n1 ← betree.Node.lookup_back n0 key st - Result.ret (betree.Internal.mk i i0 n n1) + let (st1, (o, n2)) ← betree.Node.lookup n1 key st + Result.ret (st1, (o, betree.Internal.mk i i1 n n2)) -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: Source: 'src/betree.rs', lines 709:4-709:58 -/ divergent def betree.Node.lookup (self : betree.Node) (key : U64) (st : State) : - Result (State × (Option U64)) + Result (State × ((Option U64) × betree.Node)) := match self with | betree.Node.Internal node => do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, msgs) ← betree.load_internal_node i st - let pending ← betree.Node.lookup_first_message_for_key key msgs - match pending with - | betree.List.Cons p l => - let (k, msg) := p - if k != key - then - do - let (st1, o) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0) - key st0 - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, msg) l) - Result.ret (st1, o) - else - match msg with - | betree.Message.Insert v => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Insert v) l) - Result.ret (st0, some v) - | betree.Message.Delete => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Delete) l) - Result.ret (st0, none) - | betree.Message.Upsert ufs => - do - let (st1, v) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n - n0) key st0 - let (st2, v0) ← - betree.Node.apply_upserts (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i - i0 n n0) key st0 - let ⟨ i1, _, _, _ ⟩ := node0 - let pending0 ← - betree.Node.apply_upserts_back (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let msgs0 ← - betree.Node.lookup_first_message_for_key_back key msgs pending0 - let (st3, _) ← betree.store_internal_node i1 msgs0 st2 - Result.ret (st3, some v0) - | betree.List.Nil => + let ⟨ i, i1, n, n1 ⟩ := node + let (st1, msgs) ← betree.load_internal_node i st + let (pending, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key msgs + match pending with + | betree.List.Cons p l => + let (k, msg) := p + if k != key + then do - let (st1, o) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0) - key st0 + let (st2, (o, i2)) ← + betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key + st1 + let _ ← + lookup_first_message_for_key_back (betree.List.Cons (k, msg) l) + Result.ret (st2, (o, betree.Node.Internal i2)) + else + match msg with + | betree.Message.Insert v => + do let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - betree.List.Nil - Result.ret (st1, o) - | betree.Node.Leaf node => - do - let (st0, bindings) ← betree.load_leaf_node node.id st - let o ← betree.Node.lookup_in_bindings key bindings - Result.ret (st0, o) - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 - Source: 'src/betree.rs', lines 709:4-709:58 -/ -divergent def betree.Node.lookup_back - (self : betree.Node) (key : U64) (st : State) : Result betree.Node := - match self with - | betree.Node.Internal node => - do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, msgs) ← betree.load_internal_node i st - let pending ← betree.Node.lookup_first_message_for_key key msgs - match pending with - | betree.List.Cons p l => - let (k, msg) := p - if k != key - then + lookup_first_message_for_key_back (betree.List.Cons (k, + betree.Message.Insert v) l) + Result.ret (st1, (some v, betree.Node.Internal (betree.Internal.mk i + i1 n n1))) + | betree.Message.Delete => do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, msg) l) - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 - n n0) key st0 - Result.ret (betree.Node.Internal node0) - else - match msg with - | betree.Message.Insert v => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Insert v) l) - Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0)) - | betree.Message.Delete => - do - let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - (betree.List.Cons (k, betree.Message.Delete) l) - Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0)) - | betree.Message.Upsert ufs => - do - let (st1, v) ← - betree.Internal.lookup_in_children (betree.Internal.mk i i0 n - n0) key st0 - let (st2, _) ← - betree.Node.apply_upserts (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i - i0 n n0) key st0 - let ⟨ i1, i2, n1, n2 ⟩ := node0 - let pending0 ← - betree.Node.apply_upserts_back (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key st1 - let msgs0 ← - betree.Node.lookup_first_message_for_key_back key msgs pending0 - let _ ← betree.store_internal_node i1 msgs0 st2 - Result.ret (betree.Node.Internal (betree.Internal.mk i1 i2 n1 - n2)) - | betree.List.Nil => - do let _ ← - betree.Node.lookup_first_message_for_key_back key msgs - betree.List.Nil - let node0 ← - betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 n - n0) key st0 - Result.ret (betree.Node.Internal node0) + lookup_first_message_for_key_back (betree.List.Cons (k, + betree.Message.Delete) l) + Result.ret (st1, (none, betree.Node.Internal (betree.Internal.mk i i1 + n n1))) + | betree.Message.Upsert ufs => + do + let (st2, (v, i2)) ← + betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) + key st1 + let (st3, (v1, l1)) ← + betree.Node.apply_upserts (betree.List.Cons (k, + betree.Message.Upsert ufs) l) v key st2 + let ⟨ i3, i4, n2, n3 ⟩ := i2 + let msgs1 ← lookup_first_message_for_key_back l1 + let (st4, _) ← betree.store_internal_node i3 msgs1 st3 + Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk + i3 i4 n2 n3))) + | betree.List.Nil => + do + let (st2, (o, i2)) ← + betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key + st1 + let _ ← lookup_first_message_for_key_back betree.List.Nil + Result.ret (st2, (o, betree.Node.Internal i2)) | betree.Node.Leaf node => do - let (_, bindings) ← betree.load_leaf_node node.id st - let _ ← betree.Node.lookup_in_bindings key bindings - Result.ret (betree.Node.Leaf node) + let (st1, bindings) ← betree.load_leaf_node node.id st + let o ← betree.Node.lookup_in_bindings key bindings + Result.ret (st1, (o, betree.Node.Leaf node)) end -/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: Source: 'src/betree.rs', lines 674:4-674:77 -/ divergent def betree.Node.filter_messages_for_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : @@ -517,33 +353,19 @@ divergent def betree.Node.filter_messages_for_key if k = key then do - let msgs0 ← - betree.List.pop_front_back (U64 × betree.Message) (betree.List.Cons - (k, m) l) - betree.Node.filter_messages_for_key key msgs0 + let (_, l1) ← + betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) + l) + betree.Node.filter_messages_for_key key l1 else Result.ret (betree.List.Cons (k, m) l) | betree.List.Nil => Result.ret betree.List.Nil -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: Source: 'src/betree.rs', lines 689:4-692:34 -/ divergent def betree.Node.lookup_first_message_after_key (key : U64) (msgs : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) - := - match msgs with - | betree.List.Cons p next_msgs => - let (k, m) := p - if k = key - then betree.Node.lookup_first_message_after_key key next_msgs - else Result.ret (betree.List.Cons (k, m) next_msgs) - | betree.List.Nil => Result.ret betree.List.Nil - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 - Source: 'src/betree.rs', lines 689:4-692:34 -/ -divergent def betree.Node.lookup_first_message_after_key_back - (key : U64) (msgs : betree.List (U64 × betree.Message)) - (ret : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) + Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 × + betree.Message) → Result (betree.List (U64 × betree.Message)))) := match msgs with | betree.List.Cons p next_msgs => @@ -551,14 +373,22 @@ divergent def betree.Node.lookup_first_message_after_key_back if k = key then do - let next_msgs0 ← - betree.Node.lookup_first_message_after_key_back key next_msgs ret - Result.ret (betree.List.Cons (k, m) next_msgs0) - else Result.ret ret - | betree.List.Nil => Result.ret ret + let (l, lookup_first_message_after_key_back) ← + betree.Node.lookup_first_message_after_key key next_msgs + let back_'a := + fun ret => + do + let next_msgs1 ← lookup_first_message_after_key_back ret + Result.ret (betree.List.Cons (k, m) next_msgs1) + Result.ret (l, back_'a) + else + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Cons (k, m) next_msgs, back_'a) + | betree.List.Nil => + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Nil, back_'a) -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: Source: 'src/betree.rs', lines 521:4-521:89 -/ def betree.Node.apply_to_internal (msgs : betree.List (U64 × betree.Message)) (key : U64) @@ -566,66 +396,63 @@ def betree.Node.apply_to_internal Result (betree.List (U64 × betree.Message)) := do - let msgs0 ← betree.Node.lookup_first_message_for_key key msgs - let b ← betree.ListTupleU64T.head_has_key betree.Message msgs0 key - if b - then - match new_msg with - | betree.Message.Insert i => + let (msgs1, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key msgs + let b ← betree.ListTupleU64T.head_has_key betree.Message msgs1 key + if b + then + match new_msg with + | betree.Message.Insert i => + do + let l ← betree.Node.filter_messages_for_key key msgs1 + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Insert i) + lookup_first_message_for_key_back l1 + | betree.Message.Delete => + do + let l ← betree.Node.filter_messages_for_key key msgs1 + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Delete) + lookup_first_message_for_key_back l1 + | betree.Message.Upsert s => + do + let p ← betree.List.hd (U64 × betree.Message) msgs1 + let (_, m) := p + match m with + | betree.Message.Insert prev => do - let msgs1 ← betree.Node.filter_messages_for_key key msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Insert i) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 + let v ← betree.upsert_update (some prev) s + let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Insert v) + lookup_first_message_for_key_back l1 | betree.Message.Delete => do - let msgs1 ← betree.Node.filter_messages_for_key key msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Delete) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree.Message.Upsert s => + let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let v ← betree.upsert_update none s + let l1 ← + betree.List.push_front (U64 × betree.Message) l (key, + betree.Message.Insert v) + lookup_first_message_for_key_back l1 + | betree.Message.Upsert _ => do - let p ← betree.List.hd (U64 × betree.Message) msgs0 - let (_, m) := p - match m with - | betree.Message.Insert prev => - do - let v ← betree.upsert_update (some prev) s - let msgs1 ← - betree.List.pop_front_back (U64 × betree.Message) msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Insert v) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree.Message.Delete => - do - let v ← betree.upsert_update none s - let msgs1 ← - betree.List.pop_front_back (U64 × betree.Message) msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Insert v) - betree.Node.lookup_first_message_for_key_back key msgs msgs2 - | betree.Message.Upsert ufs => - do - let msgs1 ← - betree.Node.lookup_first_message_after_key key msgs0 - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, - betree.Message.Upsert s) - let msgs3 ← - betree.Node.lookup_first_message_after_key_back key msgs0 msgs2 - betree.Node.lookup_first_message_for_key_back key msgs msgs3 - else - do - let msgs1 ← - betree.List.push_front (U64 × betree.Message) msgs0 (key, new_msg) - betree.Node.lookup_first_message_for_key_back key msgs msgs1 + let (msgs2, lookup_first_message_after_key_back) ← + betree.Node.lookup_first_message_after_key key msgs1 + let l ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, + betree.Message.Upsert s) + let msgs3 ← lookup_first_message_after_key_back l + lookup_first_message_for_key_back msgs3 + else + do + let l ← + betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) + lookup_first_message_for_key_back l -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: Source: 'src/betree.rs', lines 502:4-505:5 -/ divergent def betree.Node.apply_messages_to_internal (msgs : betree.List (U64 × betree.Message)) @@ -635,45 +462,40 @@ divergent def betree.Node.apply_messages_to_internal match new_msgs with | betree.List.Cons new_msg new_msgs_tl => do - let (i, m) := new_msg - let msgs0 ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal msgs0 new_msgs_tl + let (i, m) := new_msg + let l ← betree.Node.apply_to_internal msgs i m + betree.Node.apply_messages_to_internal l new_msgs_tl | betree.List.Nil => Result.ret msgs -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: Source: 'src/betree.rs', lines 653:4-656:32 -/ divergent def betree.Node.lookup_mut_in_bindings (key : U64) (bindings : betree.List (U64 × U64)) : - Result (betree.List (U64 × U64)) + Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result + (betree.List (U64 × U64)))) := match bindings with | betree.List.Cons hd tl => - let (i, i0) := hd + let (i, i1) := hd if i >= key - then Result.ret (betree.List.Cons (i, i0) tl) - else betree.Node.lookup_mut_in_bindings key tl - | betree.List.Nil => Result.ret betree.List.Nil - -/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 - Source: 'src/betree.rs', lines 653:4-656:32 -/ -divergent def betree.Node.lookup_mut_in_bindings_back - (key : U64) (bindings : betree.List (U64 × U64)) - (ret : betree.List (U64 × U64)) : - Result (betree.List (U64 × U64)) - := - match bindings with - | betree.List.Cons hd tl => - let (i, i0) := hd - if i >= key - then Result.ret ret + then + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Cons (i, i1) tl, back_'a) else do - let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret - Result.ret (betree.List.Cons (i, i0) tl0) - | betree.List.Nil => Result.ret ret - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) + let (l, lookup_mut_in_bindings_back) ← + betree.Node.lookup_mut_in_bindings key tl + let back_'a := + fun ret => + do + let tl1 ← lookup_mut_in_bindings_back ret + Result.ret (betree.List.Cons (i, i1) tl1) + Result.ret (l, back_'a) + | betree.List.Nil => + let back_'a := fun ret => Result.ret ret + Result.ret (betree.List.Nil, back_'a) + +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: Source: 'src/betree.rs', lines 460:4-460:87 -/ def betree.Node.apply_to_leaf (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message) @@ -681,49 +503,39 @@ def betree.Node.apply_to_leaf Result (betree.List (U64 × U64)) := do - let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings - let b ← betree.ListTupleU64T.head_has_key U64 bindings0 key - if b - then + let (bindings1, lookup_mut_in_bindings_back) ← + betree.Node.lookup_mut_in_bindings key bindings + let b ← betree.ListTupleU64T.head_has_key U64 bindings1 key + if b + then + do + let (hd, l) ← betree.List.pop_front (U64 × U64) bindings1 + match new_msg with + | betree.Message.Insert v => do - let hd ← betree.List.pop_front (U64 × U64) bindings0 - match new_msg with - | betree.Message.Insert v => - do - let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 - let bindings2 ← - betree.List.push_front (U64 × U64) bindings1 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings2 - | betree.Message.Delete => - do - let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 - betree.Node.lookup_mut_in_bindings_back key bindings bindings1 - | betree.Message.Upsert s => - do - let (_, i) := hd - let v ← betree.upsert_update (some i) s - let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0 - let bindings2 ← - betree.List.push_front (U64 × U64) bindings1 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings2 - else - match new_msg with - | betree.Message.Insert v => - do - let bindings1 ← - betree.List.push_front (U64 × U64) bindings0 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings1 - | betree.Message.Delete => - betree.Node.lookup_mut_in_bindings_back key bindings bindings0 - | betree.Message.Upsert s => - do - let v ← betree.upsert_update none s - let bindings1 ← - betree.List.push_front (U64 × U64) bindings0 (key, v) - betree.Node.lookup_mut_in_bindings_back key bindings bindings1 + let l1 ← betree.List.push_front (U64 × U64) l (key, v) + lookup_mut_in_bindings_back l1 + | betree.Message.Delete => lookup_mut_in_bindings_back l + | betree.Message.Upsert s => + do + let (_, i) := hd + let v ← betree.upsert_update (some i) s + let l1 ← betree.List.push_front (U64 × U64) l (key, v) + lookup_mut_in_bindings_back l1 + else + match new_msg with + | betree.Message.Insert v => + do + let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back l + | betree.Message.Delete => lookup_mut_in_bindings_back bindings1 + | betree.Message.Upsert s => + do + let v ← betree.upsert_update none s + let l ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back l -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: Source: 'src/betree.rs', lines 444:4-447:5 -/ divergent def betree.Node.apply_messages_to_leaf (bindings : betree.List (U64 × U64)) @@ -733,337 +545,183 @@ divergent def betree.Node.apply_messages_to_leaf match new_msgs with | betree.List.Cons new_msg new_msgs_tl => do - let (i, m) := new_msg - let bindings0 ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl + let (i, m) := new_msg + let l ← betree.Node.apply_to_leaf bindings i m + betree.Node.apply_messages_to_leaf l new_msgs_tl | betree.List.Nil => Result.ret bindings -/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function +/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: Source: 'src/betree.rs', lines 410:4-415:26 -/ mutual divergent def betree.Internal.flush (self : betree.Internal) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (content : betree.List (U64 × betree.Message)) (st : State) : - Result (State × (betree.List (U64 × betree.Message))) - := - do - let ⟨ _, i, n, n0 ⟩ := self - let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i - let (msgs_left, msgs_right) := p - let len_left ← betree.List.len (U64 × betree.Message) msgs_left - if len_left >= params.min_flush_size - then - do - let (st0, _) ← - betree.Node.apply_messages n params node_id_cnt msgs_left st - let (_, node_id_cnt0) ← - betree.Node.apply_messages_back n params node_id_cnt msgs_left st - let len_right ← betree.List.len (U64 × betree.Message) msgs_right - if len_right >= params.min_flush_size - then - do - let (st1, _) ← - betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0 - let _ ← - betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right - st0 - Result.ret (st1, betree.List.Nil) - else Result.ret (st0, msgs_right) - else - do - let (st0, _) ← - betree.Node.apply_messages n0 params node_id_cnt msgs_right st - let _ ← - betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st - Result.ret (st0, msgs_left) - -/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 - Source: 'src/betree.rs', lines 410:4-415:26 -/ -divergent def betree.Internal.flush_back - (self : betree.Internal) (params : betree.Params) - (node_id_cnt : betree.NodeIdCounter) - (content : betree.List (U64 × betree.Message)) (st : State) : - Result (betree.Internal × betree.NodeIdCounter) + Result (State × ((betree.List (U64 × betree.Message)) × (betree.Internal + × betree.NodeIdCounter))) := do - let ⟨ i, i0, n, n0 ⟩ := self - let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i0 - let (msgs_left, msgs_right) := p - let len_left ← betree.List.len (U64 × betree.Message) msgs_left - if len_left >= params.min_flush_size + let ⟨ i, i1, n, n1 ⟩ := self + let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i1 + let (msgs_left, msgs_right) := p + let len_left ← betree.List.len (U64 × betree.Message) msgs_left + if len_left >= params.min_flush_size + then + do + let (st1, p1) ← + betree.Node.apply_messages n params node_id_cnt msgs_left st + let (n2, node_id_cnt1) := p1 + let len_right ← betree.List.len (U64 × betree.Message) msgs_right + if len_right >= params.min_flush_size then do - let (st0, _) ← - betree.Node.apply_messages n params node_id_cnt msgs_left st - let (n1, node_id_cnt0) ← - betree.Node.apply_messages_back n params node_id_cnt msgs_left st - let len_right ← betree.List.len (U64 × betree.Message) msgs_right - if len_right >= params.min_flush_size - then - do - let (n2, node_id_cnt1) ← - betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right - st0 - Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1) - else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0) + let (st2, p2) ← + betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1 + let (n3, node_id_cnt2) := p2 + Result.ret (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3, + node_id_cnt2))) else - do - let (n1, node_id_cnt0) ← - betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st - Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0) - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function - Source: 'src/betree.rs', lines 588:4-593:5 -/ -divergent def betree.Node.apply_messages - (self : betree.Node) (params : betree.Params) - (node_id_cnt : betree.NodeIdCounter) - (msgs : betree.List (U64 × betree.Message)) (st : State) : - Result (State × Unit) - := - match self with - | betree.Node.Internal node => - do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, content) ← betree.load_internal_node i st - let content0 ← betree.Node.apply_messages_to_internal content msgs - let num_msgs ← betree.List.len (U64 × betree.Message) content0 - if num_msgs >= params.min_flush_size - then - do - let (st1, content1) ← - betree.Internal.flush (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let (node0, _) ← - betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let ⟨ i1, _, _, _ ⟩ := node0 - let (st2, _) ← betree.store_internal_node i1 content1 st1 - Result.ret (st2, ()) - else - do - let (st1, _) ← betree.store_internal_node i content0 st0 - Result.ret (st1, ()) - | betree.Node.Leaf node => + Result.ret (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1, + node_id_cnt1))) + else do - let (st0, content) ← betree.load_leaf_node node.id st - let content0 ← betree.Node.apply_messages_to_leaf content msgs - let len ← betree.List.len (U64 × U64) content0 - let i ← 2#u64 * params.split_size - if len >= i - then - do - let (st1, _) ← - betree.Leaf.split node content0 params node_id_cnt st0 - let (st2, _) ← betree.store_leaf_node node.id betree.List.Nil st1 - Result.ret (st2, ()) - else - do - let (st1, _) ← betree.store_leaf_node node.id content0 st0 - Result.ret (st1, ()) + let (st1, p1) ← + betree.Node.apply_messages n1 params node_id_cnt msgs_right st + let (n2, node_id_cnt1) := p1 + Result.ret (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1))) -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 +/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: Source: 'src/betree.rs', lines 588:4-593:5 -/ -divergent def betree.Node.apply_messages_back +divergent def betree.Node.apply_messages (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (msgs : betree.List (U64 × betree.Message)) (st : State) : - Result (betree.Node × betree.NodeIdCounter) + Result (State × (betree.Node × betree.NodeIdCounter)) := match self with | betree.Node.Internal node => do - let ⟨ i, i0, n, n0 ⟩ := node - let (st0, content) ← betree.load_internal_node i st - let content0 ← betree.Node.apply_messages_to_internal content msgs - let num_msgs ← betree.List.len (U64 × betree.Message) content0 - if num_msgs >= params.min_flush_size - then - do - let (st1, content1) ← - betree.Internal.flush (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let (node0, node_id_cnt0) ← - betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params - node_id_cnt content0 st0 - let ⟨ i1, i2, n1, n2 ⟩ := node0 - let _ ← betree.store_internal_node i1 content1 st1 - Result.ret (betree.Node.Internal (betree.Internal.mk i1 i2 n1 n2), - node_id_cnt0) - else - do - let _ ← betree.store_internal_node i content0 st0 - Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0), - node_id_cnt) + let ⟨ i, i1, n, n1 ⟩ := node + let (st1, content) ← betree.load_internal_node i st + let l ← betree.Node.apply_messages_to_internal content msgs + let num_msgs ← betree.List.len (U64 × betree.Message) l + if num_msgs >= params.min_flush_size + then + do + let (st2, (content1, p)) ← + betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt + l st1 + let (node1, node_id_cnt1) := p + let ⟨ i2, i3, n2, n3 ⟩ := node1 + let (st3, _) ← betree.store_internal_node i2 content1 st2 + Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3), + node_id_cnt1)) + else + do + let (st2, _) ← betree.store_internal_node i l st1 + Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1), + node_id_cnt)) | betree.Node.Leaf node => do - let (st0, content) ← betree.load_leaf_node node.id st - let content0 ← betree.Node.apply_messages_to_leaf content msgs - let len ← betree.List.len (U64 × U64) content0 - let i ← 2#u64 * params.split_size - if len >= i - then - do - let (st1, new_node) ← - betree.Leaf.split node content0 params node_id_cnt st0 - let _ ← betree.store_leaf_node node.id betree.List.Nil st1 - let node_id_cnt0 ← - betree.Leaf.split_back node content0 params node_id_cnt st0 - Result.ret (betree.Node.Internal new_node, node_id_cnt0) - else - do - let _ ← betree.store_leaf_node node.id content0 st0 - Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt) + let (st1, content) ← betree.load_leaf_node node.id st + let l ← betree.Node.apply_messages_to_leaf content msgs + let len ← betree.List.len (U64 × U64) l + let i ← 2#u64 * params.split_size + if len >= i + then + do + let (st2, (new_node, nic)) ← + betree.Leaf.split node l params node_id_cnt st1 + let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2 + Result.ret (st3, (betree.Node.Internal new_node, nic)) + else + do + let (st2, _) ← betree.store_leaf_node node.id l st1 + Result.ret (st2, (betree.Node.Leaf { node with size := len }, + node_id_cnt)) end -/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function +/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: Source: 'src/betree.rs', lines 576:4-582:5 -/ def betree.Node.apply (self : betree.Node) (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) (st : State) : - Result (State × Unit) + Result (State × (betree.Node × betree.NodeIdCounter)) := do - let l := betree.List.Nil - let (st0, _) ← - betree.Node.apply_messages self params node_id_cnt (betree.List.Cons - (key, new_msg) l) st - let _ ← - betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons - (key, new_msg) l) st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 - Source: 'src/betree.rs', lines 576:4-582:5 -/ -def betree.Node.apply_back - (self : betree.Node) (params : betree.Params) - (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message) - (st : State) : - Result (betree.Node × betree.NodeIdCounter) - := let l := betree.List.Nil - betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons - (key, new_msg) l) st + let (st1, p) ← + betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key, + new_msg) l) st + let (self1, node_id_cnt1) := p + Result.ret (st1, (self1, node_id_cnt1)) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: Source: 'src/betree.rs', lines 849:4-849:60 -/ def betree.BeTree.new (min_flush_size : U64) (split_size : U64) (st : State) : Result (State × betree.BeTree) := do - let node_id_cnt ← betree.NodeIdCounter.new - let id ← betree.NodeIdCounter.fresh_id node_id_cnt - let (st0, _) ← betree.store_leaf_node id betree.List.Nil st - let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt - Result.ret (st0, - { - params := - { min_flush_size := min_flush_size, split_size := split_size }, - node_id_cnt := node_id_cnt0, - root := (betree.Node.Leaf { id := id, size := 0#u64 }) - }) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function + let node_id_cnt ← betree.NodeIdCounter.new + let (id, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (st1, _) ← betree.store_leaf_node id betree.List.Nil st + Result.ret (st1, + { + params := { min_flush_size := min_flush_size, split_size := split_size }, + node_id_cnt := nic, + root := (betree.Node.Leaf { id := id, size := 0#u64 }) + }) + +/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: Source: 'src/betree.rs', lines 868:4-868:47 -/ def betree.BeTree.apply (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : - Result (State × Unit) - := - do - let (st0, _) ← - betree.Node.apply self.root self.params self.node_id_cnt key msg st - let _ ← - betree.Node.apply_back self.root self.params self.node_id_cnt key msg st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 - Source: 'src/betree.rs', lines 868:4-868:47 -/ -def betree.BeTree.apply_back - (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) : - Result betree.BeTree + Result (State × betree.BeTree) := do - let (n, nic) ← - betree.Node.apply_back self.root self.params self.node_id_cnt key msg st - Result.ret { self with node_id_cnt := nic, root := n } + let (st1, p) ← + betree.Node.apply self.root self.params self.node_id_cnt key msg st + let (n, nic) := p + Result.ret (st1, { self with node_id_cnt := nic, root := n }) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: Source: 'src/betree.rs', lines 874:4-874:52 -/ def betree.BeTree.insert (self : betree.BeTree) (key : U64) (value : U64) (st : State) : - Result (State × Unit) - := - do - let (st0, _) ← - betree.BeTree.apply self key (betree.Message.Insert value) st - let _ ← - betree.BeTree.apply_back self key (betree.Message.Insert value) st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 - Source: 'src/betree.rs', lines 874:4-874:52 -/ -def betree.BeTree.insert_back - (self : betree.BeTree) (key : U64) (value : U64) (st : State) : - Result betree.BeTree + Result (State × betree.BeTree) := - betree.BeTree.apply_back self key (betree.Message.Insert value) st + betree.BeTree.apply self key (betree.Message.Insert value) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: Source: 'src/betree.rs', lines 880:4-880:38 -/ def betree.BeTree.delete - (self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) := - do - let (st0, _) ← betree.BeTree.apply self key betree.Message.Delete st - let _ ← betree.BeTree.apply_back self key betree.Message.Delete st - Result.ret (st0, ()) - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 - Source: 'src/betree.rs', lines 880:4-880:38 -/ -def betree.BeTree.delete_back - (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree := - betree.BeTree.apply_back self key betree.Message.Delete st - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function - Source: 'src/betree.rs', lines 886:4-886:59 -/ -def betree.BeTree.upsert - (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) - : - Result (State × Unit) + (self : betree.BeTree) (key : U64) (st : State) : + Result (State × betree.BeTree) := - do - let (st0, _) ← - betree.BeTree.apply self key (betree.Message.Upsert upd) st - let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st - Result.ret (st0, ()) + betree.BeTree.apply self key betree.Message.Delete st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 +/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: Source: 'src/betree.rs', lines 886:4-886:59 -/ -def betree.BeTree.upsert_back +def betree.BeTree.upsert (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State) : - Result betree.BeTree + Result (State × betree.BeTree) := - betree.BeTree.apply_back self key (betree.Message.Upsert upd) st + betree.BeTree.apply self key (betree.Message.Upsert upd) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function +/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: Source: 'src/betree.rs', lines 895:4-895:62 -/ def betree.BeTree.lookup (self : betree.BeTree) (key : U64) (st : State) : - Result (State × (Option U64)) + Result (State × ((Option U64) × betree.BeTree)) := - betree.Node.lookup self.root key st - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 - Source: 'src/betree.rs', lines 895:4-895:62 -/ -def betree.BeTree.lookup_back - (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree := do - let n ← betree.Node.lookup_back self.root key st - Result.ret { self with root := n } + let (st1, (o, n)) ← betree.Node.lookup self.root key st + Result.ret (st1, (o, { self with root := n })) -/- [betree_main::main]: forward function +/- [betree_main::main]: Source: 'src/betree_main.rs', lines 5:0-5:9 -/ def main : Result Unit := Result.ret () diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean index 95f88873..eaa4b6c2 100644 --- a/tests/lean/BetreeMain/FunsExternal_Template.lean +++ b/tests/lean/BetreeMain/FunsExternal_Template.lean @@ -6,29 +6,29 @@ import BetreeMain.Types open Primitives open betree_main -/- [betree_main::betree_utils::load_internal_node]: forward function +/- [betree_main::betree_utils::load_internal_node]: Source: 'src/betree_utils.rs', lines 98:0-98:63 -/ axiom betree_utils.load_internal_node : U64 → State → Result (State × (betree.List (U64 × betree.Message))) -/- [betree_main::betree_utils::store_internal_node]: forward function +/- [betree_main::betree_utils::store_internal_node]: Source: 'src/betree_utils.rs', lines 115:0-115:71 -/ axiom betree_utils.store_internal_node : U64 → betree.List (U64 × betree.Message) → State → Result (State × Unit) -/- [betree_main::betree_utils::load_leaf_node]: forward function +/- [betree_main::betree_utils::load_leaf_node]: Source: 'src/betree_utils.rs', lines 132:0-132:55 -/ axiom betree_utils.load_leaf_node : U64 → State → Result (State × (betree.List (U64 × U64))) -/- [betree_main::betree_utils::store_leaf_node]: forward function +/- [betree_main::betree_utils::store_leaf_node]: Source: 'src/betree_utils.rs', lines 145:0-145:63 -/ axiom betree_utils.store_leaf_node : U64 → betree.List (U64 × U64) → State → Result (State × Unit) -/- [core::option::{core::option::Option<T>}::unwrap]: forward function +/- [core::option::{core::option::Option<T>}::unwrap]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/ axiom core.option.Option.unwrap (T : Type) : Option T → State → Result (State × T) diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean index c8538aa2..7c47e3dd 100644 --- a/tests/lean/Bitwise.lean +++ b/tests/lean/Bitwise.lean @@ -5,31 +5,31 @@ open Primitives namespace bitwise -/- [bitwise::shift_u32]: forward function +/- [bitwise::shift_u32]: Source: 'src/bitwise.rs', lines 3:0-3:31 -/ def shift_u32 (a : U32) : Result U32 := do - let t ← a >>> 16#usize - t <<< 16#usize + let t ← a >>> 16#usize + t <<< 16#usize -/- [bitwise::shift_i32]: forward function +/- [bitwise::shift_i32]: Source: 'src/bitwise.rs', lines 10:0-10:31 -/ def shift_i32 (a : I32) : Result I32 := do - let t ← a >>> 16#isize - t <<< 16#isize + let t ← a >>> 16#isize + t <<< 16#isize -/- [bitwise::xor_u32]: forward function +/- [bitwise::xor_u32]: Source: 'src/bitwise.rs', lines 17:0-17:37 -/ def xor_u32 (a : U32) (b : U32) : Result U32 := Result.ret (a ^^^ b) -/- [bitwise::or_u32]: forward function +/- [bitwise::or_u32]: Source: 'src/bitwise.rs', lines 21:0-21:36 -/ def or_u32 (a : U32) (b : U32) : Result U32 := Result.ret (a ||| b) -/- [bitwise::and_u32]: forward function +/- [bitwise::and_u32]: Source: 'src/bitwise.rs', lines 25:0-25:37 -/ def and_u32 (a : U32) (b : U32) : Result U32 := Result.ret (a &&& b) diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index 80864427..2912805f 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -20,7 +20,7 @@ def x1_c : U32 := eval_global x1_body (by simp) def x2_body : Result U32 := Result.ret 3#u32 def x2_c : U32 := eval_global x2_body (by simp) -/- [constants::incr]: forward function +/- [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 -/ def incr (n : U32) : Result U32 := n + 1#u32 @@ -30,7 +30,7 @@ def incr (n : U32) : Result U32 := def x3_body : Result U32 := incr 32#u32 def x3_c : U32 := eval_global x3_body (by simp) -/- [constants::mk_pair0]: forward function +/- [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 -/ def mk_pair0 (x : U32) (y : U32) : Result (U32 × U32) := Result.ret (x, y) @@ -41,7 +41,7 @@ structure Pair (T1 T2 : Type) where x : T1 y : T2 -/- [constants::mk_pair1]: forward function +/- [constants::mk_pair1]: Source: 'src/constants.rs', lines 27:0-27:55 -/ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) := Result.ret { x := x, y := y } @@ -71,7 +71,7 @@ def p3_c : Pair U32 U32 := eval_global p3_body (by simp) structure Wrap (T : Type) where value : T -/- [constants::{constants::Wrap<T>}::new]: forward function +/- [constants::{constants::Wrap<T>}::new]: Source: 'src/constants.rs', lines 54:4-54:41 -/ def Wrap.new (T : Type) (value : T) : Result (Wrap T) := Result.ret { value := value } @@ -81,7 +81,7 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) := def y_body : Result (Wrap I32) := Wrap.new I32 2#i32 def y_c : Wrap I32 := eval_global y_body (by simp) -/- [constants::unwrap_y]: forward function +/- [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 -/ def unwrap_y : Result I32 := Result.ret y_c.value @@ -96,12 +96,12 @@ def yval_c : I32 := eval_global yval_body (by simp) def get_z1_z1_body : Result I32 := Result.ret 3#i32 def get_z1_z1_c : I32 := eval_global get_z1_z1_body (by simp) -/- [constants::get_z1]: forward function +/- [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 -/ def get_z1 : Result I32 := Result.ret get_z1_z1_c -/- [constants::add]: forward function +/- [constants::add]: Source: 'src/constants.rs', lines 66:0-66:39 -/ def add (a : I32) (b : I32) : Result I32 := a + b @@ -121,13 +121,13 @@ def q2_c : I32 := eval_global q2_body (by simp) def q3_body : Result I32 := add q2_c 3#i32 def q3_c : I32 := eval_global q3_body (by simp) -/- [constants::get_z2]: forward function +/- [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 -/ def get_z2 : Result I32 := do - let i ← get_z1 - let i0 ← add i q3_c - add q1_c i0 + let i ← get_z1 + let i1 ← add i q3_c + add q1_c i1 /- [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 -/ diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 48ec6ad5..88ced82d 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -7,92 +7,59 @@ open Primitives namespace external -/- [external::swap]: forward function +/- [external::swap]: Source: 'src/external.rs', lines 6:0-6:46 -/ -def swap (T : Type) (x : T) (y : T) (st : State) : Result (State × Unit) := - do - let (st0, _) ← core.mem.swap T x y st - let (st1, _) ← core.mem.swap_back0 T x y st st0 - let (st2, _) ← core.mem.swap_back1 T x y st st1 - Result.ret (st2, ()) - -/- [external::swap]: backward function 0 - Source: 'src/external.rs', lines 6:0-6:46 -/ -def swap_back - (T : Type) (x : T) (y : T) (st : State) (st0 : State) : - Result (State × (T × T)) - := - do - let (st1, _) ← core.mem.swap T x y st - let (st2, x0) ← core.mem.swap_back0 T x y st st1 - let (_, y0) ← core.mem.swap_back1 T x y st st2 - Result.ret (st0, (x0, y0)) +def swap + (T : Type) (x : T) (y : T) (st : State) : Result (State × (T × T)) := + core.mem.swap T x y st -/- [external::test_new_non_zero_u32]: forward function +/- [external::test_new_non_zero_u32]: Source: 'src/external.rs', lines 11:0-11:60 -/ def test_new_non_zero_u32 (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) := do - let (st0, o) ← core.num.nonzero.NonZeroU32.new x st - core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st0 + let (st1, o) ← core.num.nonzero.NonZeroU32.new x st + core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st1 -/- [external::test_vec]: forward function +/- [external::test_vec]: Source: 'src/external.rs', lines 17:0-17:17 -/ def test_vec : Result Unit := do - let v := alloc.vec.Vec.new U32 - let _ ← alloc.vec.Vec.push U32 v 0#u32 - Result.ret () + let v := alloc.vec.Vec.new U32 + let _ ← alloc.vec.Vec.push U32 v 0#u32 + Result.ret () /- Unit test for [external::test_vec] -/ #assert (test_vec == Result.ret ()) -/- [external::custom_swap]: forward function +/- [external::custom_swap]: Source: 'src/external.rs', lines 24:0-24:66 -/ def custom_swap - (T : Type) (x : T) (y : T) (st : State) : Result (State × T) := - do - let (st0, _) ← core.mem.swap T x y st - let (st1, x0) ← core.mem.swap_back0 T x y st st0 - let (st2, _) ← core.mem.swap_back1 T x y st st1 - Result.ret (st2, x0) - -/- [external::custom_swap]: backward function 0 - Source: 'src/external.rs', lines 24:0-24:66 -/ -def custom_swap_back - (T : Type) (x : T) (y : T) (st : State) (ret : T) (st0 : State) : - Result (State × (T × T)) + (T : Type) (x : T) (y : T) (st : State) : + Result (State × (T × (T → State → Result (State × (T × T))))) := do - let (st1, _) ← core.mem.swap T x y st - let (st2, _) ← core.mem.swap_back0 T x y st st1 - let (_, y0) ← core.mem.swap_back1 T x y st st2 - Result.ret (st0, (ret, y0)) + let (st1, (t, t1)) ← core.mem.swap T x y st + let back_'a := fun ret st2 => Result.ret (st2, (ret, t1)) + Result.ret (st1, (t, back_'a)) -/- [external::test_custom_swap]: forward function +/- [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 -/ def test_custom_swap - (x : U32) (y : U32) (st : State) : Result (State × Unit) := + (x : U32) (y : U32) (st : State) : Result (State × (U32 × U32)) := do - let (st0, _) ← custom_swap U32 x y st - Result.ret (st0, ()) - -/- [external::test_custom_swap]: backward function 0 - Source: 'src/external.rs', lines 29:0-29:59 -/ -def test_custom_swap_back - (x : U32) (y : U32) (st : State) (st0 : State) : - Result (State × (U32 × U32)) - := - custom_swap_back U32 x y st 1#u32 st0 + let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st + let (_, (x1, y1)) ← custom_swap_back 1#u32 st1 + Result.ret (st1, (x1, y1)) -/- [external::test_swap_non_zero]: forward function +/- [external::test_swap_non_zero]: Source: 'src/external.rs', lines 35:0-35:44 -/ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) := do - let (st0, _) ← swap U32 x 0#u32 st - let (st1, (x0, _)) ← swap_back U32 x 0#u32 st st0 - if x0 = 0#u32 - then Result.fail .panic - else Result.ret (st1, x0) + let (st1, p) ← swap U32 x 0#u32 st + let (x1, _) := p + if x1 = 0#u32 + then Result.fail .panic + else Result.ret (st1, x1) end external diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index 55cd6bb5..7e237369 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -6,26 +6,17 @@ import External.Types open Primitives open external -/- [core::mem::swap]: forward function +/- [core::mem::swap]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ -axiom core.mem.swap (T : Type) : T → T → State → Result (State × Unit) +axiom core.mem.swap + (T : Type) : T → T → State → Result (State × (T × T)) -/- [core::mem::swap]: backward function 0 - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ -axiom core.mem.swap_back0 - (T : Type) : T → T → State → State → Result (State × T) - -/- [core::mem::swap]: backward function 1 - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/ -axiom core.mem.swap_back1 - (T : Type) : T → T → State → State → Result (State × T) - -/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function +/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/ axiom core.num.nonzero.NonZeroU32.new : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32)) -/- [core::option::{core::option::Option<T>}::unwrap]: forward function +/- [core::option::{core::option::Option<T>}::unwrap]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/ axiom core.option.Option.unwrap (T : Type) : Option T → State → Result (State × T) diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index e03981a2..32ed2b33 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -6,12 +6,12 @@ open Primitives namespace hashmap -/- [hashmap::hash_key]: forward function +/- [hashmap::hash_key]: Source: 'src/hashmap.rs', lines 27:0-27:32 -/ def hash_key (k : Usize) : Result Usize := Result.ret k -/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0: forward function +/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0: Source: 'src/hashmap.rs', lines 50:4-56:5 -/ divergent def HashMap.allocate_slots_loop (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) : @@ -20,12 +20,12 @@ divergent def HashMap.allocate_slots_loop if n > 0#usize then do - let slots0 ← alloc.vec.Vec.push (List T) slots List.Nil - let n0 ← n - 1#usize - HashMap.allocate_slots_loop T slots0 n0 + let v ← alloc.vec.Vec.push (List T) slots List.Nil + let n1 ← n - 1#usize + HashMap.allocate_slots_loop T v n1 else Result.ret slots -/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: forward function +/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: Source: 'src/hashmap.rs', lines 50:4-50:76 -/ def HashMap.allocate_slots (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) : @@ -33,7 +33,7 @@ def HashMap.allocate_slots := HashMap.allocate_slots_loop T slots n -/- [hashmap::{hashmap::HashMap<T>}::new_with_capacity]: forward function +/- [hashmap::{hashmap::HashMap<T>}::new_with_capacity]: Source: 'src/hashmap.rs', lines 59:4-63:13 -/ def HashMap.new_with_capacity (T : Type) (capacity : Usize) (max_load_dividend : Usize) @@ -41,252 +41,222 @@ def HashMap.new_with_capacity Result (HashMap T) := do - let v := alloc.vec.Vec.new (List T) - let slots ← HashMap.allocate_slots T v capacity - let i ← capacity * max_load_dividend - let i0 ← i / max_load_divisor - Result.ret - { - num_entries := 0#usize, - max_load_factor := (max_load_dividend, max_load_divisor), - max_load := i0, - slots := slots - } - -/- [hashmap::{hashmap::HashMap<T>}::new]: forward function + let v := alloc.vec.Vec.new (List T) + let slots ← HashMap.allocate_slots T v capacity + let i ← capacity * max_load_dividend + let i1 ← i / max_load_divisor + Result.ret + { + num_entries := 0#usize, + max_load_factor := (max_load_dividend, max_load_divisor), + max_load := i1, + slots := slots + } + +/- [hashmap::{hashmap::HashMap<T>}::new]: Source: 'src/hashmap.rs', lines 75:4-75:24 -/ def HashMap.new (T : Type) : Result (HashMap T) := HashMap.new_with_capacity T 32#usize 4#usize 5#usize -/- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0: Source: 'src/hashmap.rs', lines 80:4-88:5 -/ divergent def HashMap.clear_loop (T : Type) (slots : alloc.vec.Vec (List T)) (i : Usize) : Result (alloc.vec.Vec (List T)) := - let i0 := alloc.vec.Vec.len (List T) slots - if i < i0 + let i1 := alloc.vec.Vec.len (List T) slots + if i < i1 then do - let i1 ← i + 1#usize - let slots0 ← - alloc.vec.Vec.index_mut_back (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i - List.Nil - HashMap.clear_loop T slots0 i1 + let (_, index_mut_back) ← + alloc.vec.Vec.index_mut (List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i + let i2 ← i + 1#usize + let slots1 ← index_mut_back List.Nil + HashMap.clear_loop T slots1 i2 else Result.ret slots -/- [hashmap::{hashmap::HashMap<T>}::clear]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap::{hashmap::HashMap<T>}::clear]: Source: 'src/hashmap.rs', lines 80:4-80:27 -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let v ← HashMap.clear_loop T self.slots 0#usize - Result.ret { self with num_entries := 0#usize, slots := v } + let back ← HashMap.clear_loop T self.slots 0#usize + Result.ret { self with num_entries := 0#usize, slots := back } -/- [hashmap::{hashmap::HashMap<T>}::len]: forward function +/- [hashmap::{hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 -/ def HashMap.len (T : Type) (self : HashMap T) : Result Usize := Result.ret self.num_entries -/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0: forward function +/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0: Source: 'src/hashmap.rs', lines 97:4-114:5 -/ divergent def HashMap.insert_in_list_loop - (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := - match ls with - | List.Cons ckey cvalue tl => - if ckey = key - then Result.ret false - else HashMap.insert_in_list_loop T key value tl - | List.Nil => Result.ret true - -/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: forward function - Source: 'src/hashmap.rs', lines 97:4-97:71 -/ -def HashMap.insert_in_list - (T : Type) (key : Usize) (value : T) (ls : List T) : Result Bool := - HashMap.insert_in_list_loop T key value ls - -/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0: backward function 0 - Source: 'src/hashmap.rs', lines 97:4-114:5 -/ -divergent def HashMap.insert_in_list_loop_back - (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := + (T : Type) (key : Usize) (value : T) (ls : List T) : + Result (Bool × (List T)) + := match ls with | List.Cons ckey cvalue tl => if ckey = key - then Result.ret (List.Cons ckey value tl) + then Result.ret (false, List.Cons ckey value tl) else do - let tl0 ← HashMap.insert_in_list_loop_back T key value tl - Result.ret (List.Cons ckey cvalue tl0) + let (b, back) ← HashMap.insert_in_list_loop T key value tl + Result.ret (b, List.Cons ckey cvalue back) | List.Nil => let l := List.Nil - Result.ret (List.Cons key value l) + Result.ret (true, List.Cons key value l) -/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: backward function 0 +/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: Source: 'src/hashmap.rs', lines 97:4-97:71 -/ -def HashMap.insert_in_list_back - (T : Type) (key : Usize) (value : T) (ls : List T) : Result (List T) := - HashMap.insert_in_list_loop_back T key value ls +def HashMap.insert_in_list + (T : Type) (key : Usize) (value : T) (ls : List T) : + Result (Bool × (List T)) + := + HashMap.insert_in_list_loop T key value ls -/- [hashmap::{hashmap::HashMap<T>}::insert_no_resize]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap::{hashmap::HashMap<T>}::insert_no_resize]: Source: 'src/hashmap.rs', lines 117:4-117:54 -/ def HashMap.insert_no_resize (T : Type) (self : HashMap T) (key : Usize) (value : T) : Result (HashMap T) := do - let hash ← hash_key key - let i := alloc.vec.Vec.len (List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod - let inserted ← HashMap.insert_in_list T key value l - if inserted - then - do - let i0 ← self.num_entries + 1#usize - let l0 ← HashMap.insert_in_list_back T key value l - let v ← - alloc.vec.Vec.index_mut_back (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod l0 - Result.ret { self with num_entries := i0, slots := v } - else - do - let l0 ← HashMap.insert_in_list_back T key value l - let v ← - alloc.vec.Vec.index_mut_back (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod l0 - Result.ret { self with slots := v } - -/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) + let hash ← hash_key key + let i := alloc.vec.Vec.len (List T) self.slots + let hash_mod ← hash % i + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod + let (inserted, l1) ← HashMap.insert_in_list T key value l + if inserted + then + do + let i1 ← self.num_entries + 1#usize + let v ← index_mut_back l1 + Result.ret { self with num_entries := i1, slots := v } + else do + let v ← index_mut_back l1 + Result.ret { self with slots := v } + +/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0: Source: 'src/hashmap.rs', lines 183:4-196:5 -/ divergent def HashMap.move_elements_from_list_loop (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := match ls with | List.Cons k v tl => do - let ntable0 ← HashMap.insert_no_resize T ntable k v - HashMap.move_elements_from_list_loop T ntable0 tl + let hm ← HashMap.insert_no_resize T ntable k v + HashMap.move_elements_from_list_loop T hm tl | List.Nil => Result.ret ntable -/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: Source: 'src/hashmap.rs', lines 183:4-183:72 -/ def HashMap.move_elements_from_list (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := HashMap.move_elements_from_list_loop T ntable ls -/- [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0: Source: 'src/hashmap.rs', lines 171:4-180:5 -/ divergent def HashMap.move_elements_loop (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize) : Result ((HashMap T) × (alloc.vec.Vec (List T))) := - let i0 := alloc.vec.Vec.len (List T) slots - if i < i0 + let i1 := alloc.vec.Vec.len (List T) slots + if i < i1 then do - let l ← - alloc.vec.Vec.index_mut (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i - let ls := core.mem.replace (List T) l List.Nil - let ntable0 ← HashMap.move_elements_from_list T ntable ls - let i1 ← i + 1#usize - let l0 := core.mem.replace_back (List T) l List.Nil - let slots0 ← - alloc.vec.Vec.index_mut_back (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i l0 - HashMap.move_elements_loop T ntable0 slots0 i1 + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i + let (ls, l1) := core.mem.replace (List T) l List.Nil + let hm ← HashMap.move_elements_from_list T ntable ls + let i2 ← i + 1#usize + let slots1 ← index_mut_back l1 + let back_'a ← HashMap.move_elements_loop T hm slots1 i2 + let (hm1, v) := back_'a + Result.ret (hm1, v) else Result.ret (ntable, slots) -/- [hashmap::{hashmap::HashMap<T>}::move_elements]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap::{hashmap::HashMap<T>}::move_elements]: Source: 'src/hashmap.rs', lines 171:4-171:95 -/ def HashMap.move_elements (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize) : Result ((HashMap T) × (alloc.vec.Vec (List T))) := - HashMap.move_elements_loop T ntable slots i + do + let back_'a ← HashMap.move_elements_loop T ntable slots i + let (hm, v) := back_'a + Result.ret (hm, v) -/- [hashmap::{hashmap::HashMap<T>}::try_resize]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap::{hashmap::HashMap<T>}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 -/ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do - let max_usize ← Scalar.cast .Usize core_u32_max - let capacity := alloc.vec.Vec.len (List T) self.slots - let n1 ← max_usize / 2#usize - let (i, i0) := self.max_load_factor - let i1 ← n1 / i - if capacity <= i1 - then - do - let i2 ← capacity * 2#usize - let ntable ← HashMap.new_with_capacity T i2 i i0 - let (ntable0, _) ← HashMap.move_elements T ntable self.slots 0#usize - Result.ret - { - ntable0 - with - num_entries := self.num_entries, max_load_factor := (i, i0) - } - else Result.ret { self with max_load_factor := (i, i0) } - -/- [hashmap::{hashmap::HashMap<T>}::insert]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) + let max_usize ← Scalar.cast .Usize core_u32_max + let capacity := alloc.vec.Vec.len (List T) self.slots + let n1 ← max_usize / 2#usize + let (i, i1) := self.max_load_factor + let i2 ← n1 / i + if capacity <= i2 + then + do + let i3 ← capacity * 2#usize + let ntable ← HashMap.new_with_capacity T i3 i i1 + let p ← HashMap.move_elements T ntable self.slots 0#usize + let (ntable1, _) := p + Result.ret + { + ntable1 + with + num_entries := self.num_entries, max_load_factor := (i, i1) + } + else Result.ret { self with max_load_factor := (i, i1) } + +/- [hashmap::{hashmap::HashMap<T>}::insert]: Source: 'src/hashmap.rs', lines 129:4-129:48 -/ def HashMap.insert (T : Type) (self : HashMap T) (key : Usize) (value : T) : Result (HashMap T) := do - let self0 ← HashMap.insert_no_resize T self key value - let i ← HashMap.len T self0 - if i > self0.max_load - then HashMap.try_resize T self0 - else Result.ret self0 + let hm ← HashMap.insert_no_resize T self key value + let i ← HashMap.len T hm + if i > hm.max_load + then HashMap.try_resize T hm + else Result.ret hm -/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0: forward function +/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 -/ divergent def HashMap.contains_key_in_list_loop (T : Type) (key : Usize) (ls : List T) : Result Bool := match ls with - | List.Cons ckey t tl => + | List.Cons ckey _ tl => if ckey = key then Result.ret true else HashMap.contains_key_in_list_loop T key tl | List.Nil => Result.ret false -/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: forward function +/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: Source: 'src/hashmap.rs', lines 206:4-206:68 -/ def HashMap.contains_key_in_list (T : Type) (key : Usize) (ls : List T) : Result Bool := HashMap.contains_key_in_list_loop T key ls -/- [hashmap::{hashmap::HashMap<T>}::contains_key]: forward function +/- [hashmap::{hashmap::HashMap<T>}::contains_key]: Source: 'src/hashmap.rs', lines 199:4-199:49 -/ def HashMap.contains_key (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do - let hash ← hash_key key - let i := alloc.vec.Vec.len (List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod - HashMap.contains_key_in_list T key l - -/- [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0: forward function + let hash ← hash_key key + let i := alloc.vec.Vec.len (List T) self.slots + let hash_mod ← hash % i + let l ← + alloc.vec.Vec.index (List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod + HashMap.contains_key_in_list T key l + +/- [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0: Source: 'src/hashmap.rs', lines 224:4-237:5 -/ divergent def HashMap.get_in_list_loop (T : Type) (key : Usize) (ls : List T) : Result T := @@ -297,231 +267,171 @@ divergent def HashMap.get_in_list_loop else HashMap.get_in_list_loop T key tl | List.Nil => Result.fail .panic -/- [hashmap::{hashmap::HashMap<T>}::get_in_list]: forward function +/- [hashmap::{hashmap::HashMap<T>}::get_in_list]: Source: 'src/hashmap.rs', lines 224:4-224:70 -/ def HashMap.get_in_list (T : Type) (key : Usize) (ls : List T) : Result T := HashMap.get_in_list_loop T key ls -/- [hashmap::{hashmap::HashMap<T>}::get]: forward function +/- [hashmap::{hashmap::HashMap<T>}::get]: Source: 'src/hashmap.rs', lines 239:4-239:55 -/ def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T := do - let hash ← hash_key key - let i := alloc.vec.Vec.len (List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod - HashMap.get_in_list T key l - -/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0: forward function + let hash ← hash_key key + let i := alloc.vec.Vec.len (List T) self.slots + let hash_mod ← hash % i + let l ← + alloc.vec.Vec.index (List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod + HashMap.get_in_list T key l + +/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0: Source: 'src/hashmap.rs', lines 245:4-254:5 -/ divergent def HashMap.get_mut_in_list_loop - (T : Type) (ls : List T) (key : Usize) : Result T := - match ls with - | List.Cons ckey cvalue tl => - if ckey = key - then Result.ret cvalue - else HashMap.get_mut_in_list_loop T tl key - | List.Nil => Result.fail .panic - -/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: forward function - Source: 'src/hashmap.rs', lines 245:4-245:86 -/ -def HashMap.get_mut_in_list - (T : Type) (ls : List T) (key : Usize) : Result T := - HashMap.get_mut_in_list_loop T ls key - -/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0 - Source: 'src/hashmap.rs', lines 245:4-254:5 -/ -divergent def HashMap.get_mut_in_list_loop_back - (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) := + (T : Type) (ls : List T) (key : Usize) : + Result (T × (T → Result (List T))) + := match ls with | List.Cons ckey cvalue tl => if ckey = key - then Result.ret (List.Cons ckey ret tl) + then + let back_'a := fun ret => Result.ret (List.Cons ckey ret tl) + Result.ret (cvalue, back_'a) else do - let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret - Result.ret (List.Cons ckey cvalue tl0) + let (t, back_'a) ← HashMap.get_mut_in_list_loop T tl key + let back_'a1 := + fun ret => + do + let tl1 ← back_'a ret + Result.ret (List.Cons ckey cvalue tl1) + Result.ret (t, back_'a1) | List.Nil => Result.fail .panic -/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: backward function 0 +/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: Source: 'src/hashmap.rs', lines 245:4-245:86 -/ -def HashMap.get_mut_in_list_back - (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) := - HashMap.get_mut_in_list_loop_back T ls key ret - -/- [hashmap::{hashmap::HashMap<T>}::get_mut]: forward function - Source: 'src/hashmap.rs', lines 257:4-257:67 -/ -def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T := +def HashMap.get_mut_in_list + (T : Type) (ls : List T) (key : Usize) : + Result (T × (T → Result (List T))) + := do - let hash ← hash_key key - let i := alloc.vec.Vec.len (List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod - HashMap.get_mut_in_list T l key + let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key + let back_'a1 := fun ret => back_'a ret + Result.ret (t, back_'a1) -/- [hashmap::{hashmap::HashMap<T>}::get_mut]: backward function 0 +/- [hashmap::{hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 -/ -def HashMap.get_mut_back - (T : Type) (self : HashMap T) (key : Usize) (ret : T) : Result (HashMap T) := +def HashMap.get_mut + (T : Type) (self : HashMap T) (key : Usize) : + Result (T × (T → Result (HashMap T))) + := do - let hash ← hash_key key - let i := alloc.vec.Vec.len (List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod - let l0 ← HashMap.get_mut_in_list_back T l key ret - let v ← - alloc.vec.Vec.index_mut_back (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod l0 - Result.ret { self with slots := v } - -/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0: forward function - Source: 'src/hashmap.rs', lines 265:4-291:5 -/ -divergent def HashMap.remove_from_list_loop - (T : Type) (key : Usize) (ls : List T) : Result (Option T) := - match ls with - | List.Cons ckey t tl => - if ckey = key - then - let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil - match mv_ls with - | List.Cons i cvalue tl0 => Result.ret (some cvalue) - | List.Nil => Result.fail .panic - else HashMap.remove_from_list_loop T key tl - | List.Nil => Result.ret none - -/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: forward function - Source: 'src/hashmap.rs', lines 265:4-265:69 -/ -def HashMap.remove_from_list - (T : Type) (key : Usize) (ls : List T) : Result (Option T) := - HashMap.remove_from_list_loop T key ls + let hash ← hash_key key + let i := alloc.vec.Vec.len (List T) self.slots + let hash_mod ← hash % i + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod + let (t, get_mut_in_list_back) ← HashMap.get_mut_in_list T l key + let back_'a := + fun ret => + do + let l1 ← get_mut_in_list_back ret + let v ← index_mut_back l1 + Result.ret { self with slots := v } + Result.ret (t, back_'a) -/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0: backward function 1 +/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0: Source: 'src/hashmap.rs', lines 265:4-291:5 -/ -divergent def HashMap.remove_from_list_loop_back - (T : Type) (key : Usize) (ls : List T) : Result (List T) := +divergent def HashMap.remove_from_list_loop + (T : Type) (key : Usize) (ls : List T) : Result ((Option T) × (List T)) := match ls with | List.Cons ckey t tl => if ckey = key then - let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil + let (mv_ls, _) := + core.mem.replace (List T) (List.Cons ckey t tl) List.Nil match mv_ls with - | List.Cons i cvalue tl0 => Result.ret tl0 + | List.Cons _ cvalue tl1 => Result.ret (some cvalue, tl1) | List.Nil => Result.fail .panic else do - let tl0 ← HashMap.remove_from_list_loop_back T key tl - Result.ret (List.Cons ckey t tl0) - | List.Nil => Result.ret List.Nil + let (o, back) ← HashMap.remove_from_list_loop T key tl + Result.ret (o, List.Cons ckey t back) + | List.Nil => Result.ret (none, List.Nil) -/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: backward function 1 +/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: Source: 'src/hashmap.rs', lines 265:4-265:69 -/ -def HashMap.remove_from_list_back - (T : Type) (key : Usize) (ls : List T) : Result (List T) := - HashMap.remove_from_list_loop_back T key ls +def HashMap.remove_from_list + (T : Type) (key : Usize) (ls : List T) : Result ((Option T) × (List T)) := + HashMap.remove_from_list_loop T key ls -/- [hashmap::{hashmap::HashMap<T>}::remove]: forward function +/- [hashmap::{hashmap::HashMap<T>}::remove]: Source: 'src/hashmap.rs', lines 294:4-294:52 -/ def HashMap.remove - (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) := - do - let hash ← hash_key key - let i := alloc.vec.Vec.len (List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod - let x ← HashMap.remove_from_list T key l - match x with - | none => Result.ret none - | some x0 => do - let _ ← self.num_entries - 1#usize - Result.ret (some x0) - -/- [hashmap::{hashmap::HashMap<T>}::remove]: backward function 0 - Source: 'src/hashmap.rs', lines 294:4-294:52 -/ -def HashMap.remove_back - (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) := + (T : Type) (self : HashMap T) (key : Usize) : + Result ((Option T) × (HashMap T)) + := do - let hash ← hash_key key - let i := alloc.vec.Vec.len (List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod - let x ← HashMap.remove_from_list T key l - match x with - | none => - do - let l0 ← HashMap.remove_from_list_back T key l - let v ← - alloc.vec.Vec.index_mut_back (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod l0 - Result.ret { self with slots := v } - | some x0 => - do - let i0 ← self.num_entries - 1#usize - let l0 ← HashMap.remove_from_list_back T key l - let v ← - alloc.vec.Vec.index_mut_back (List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots - hash_mod l0 - Result.ret { self with num_entries := i0, slots := v } - -/- [hashmap::test1]: forward function + let hash ← hash_key key + let i := alloc.vec.Vec.len (List T) self.slots + let hash_mod ← hash % i + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod + let (x, l1) ← HashMap.remove_from_list T key l + match x with + | none => + do + let v ← index_mut_back l1 + Result.ret (none, { self with slots := v }) + | some x1 => + do + let i1 ← self.num_entries - 1#usize + let v ← index_mut_back l1 + Result.ret (some x1, { self with num_entries := i1, slots := v }) + +/- [hashmap::test1]: Source: 'src/hashmap.rs', lines 315:0-315:10 -/ def test1 : Result Unit := do - let hm ← HashMap.new U64 - let hm0 ← HashMap.insert U64 hm 0#usize 42#u64 - let hm1 ← HashMap.insert U64 hm0 128#usize 18#u64 - let hm2 ← HashMap.insert U64 hm1 1024#usize 138#u64 - let hm3 ← HashMap.insert U64 hm2 1056#usize 256#u64 - let i ← HashMap.get U64 hm3 128#usize - if not (i = 18#u64) + let hm ← HashMap.new U64 + let hm1 ← HashMap.insert U64 hm 0#usize 42#u64 + let hm2 ← HashMap.insert U64 hm1 128#usize 18#u64 + let hm3 ← HashMap.insert U64 hm2 1024#usize 138#u64 + let hm4 ← HashMap.insert U64 hm3 1056#usize 256#u64 + let i ← HashMap.get U64 hm4 128#usize + if not (i = 18#u64) + then Result.fail .panic + else + do + let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024#usize + let hm5 ← get_mut_back 56#u64 + let i1 ← HashMap.get U64 hm5 1024#usize + if not (i1 = 56#u64) then Result.fail .panic else do - let hm4 ← HashMap.get_mut_back U64 hm3 1024#usize 56#u64 - let i0 ← HashMap.get U64 hm4 1024#usize - if not (i0 = 56#u64) + let (x, hm6) ← HashMap.remove U64 hm5 1024#usize + match x with + | none => Result.fail .panic + | some x1 => + if not (x1 = 56#u64) then Result.fail .panic else do - let x ← HashMap.remove U64 hm4 1024#usize - match x with - | none => Result.fail .panic - | some x0 => - if not (x0 = 56#u64) + let i2 ← HashMap.get U64 hm6 0#usize + if not (i2 = 42#u64) + then Result.fail .panic + else + do + let i3 ← HashMap.get U64 hm6 128#usize + if not (i3 = 18#u64) + then Result.fail .panic + else + do + let i4 ← HashMap.get U64 hm6 1056#usize + if not (i4 = 256#u64) then Result.fail .panic - else - do - let hm5 ← HashMap.remove_back U64 hm4 1024#usize - let i1 ← HashMap.get U64 hm5 0#usize - if not (i1 = 42#u64) - then Result.fail .panic - else - do - let i2 ← HashMap.get U64 hm5 128#usize - if not (i2 = 18#u64) - then Result.fail .panic - else - do - let i3 ← HashMap.get U64 hm5 1056#usize - if not (i3 = 256#u64) - then Result.fail .panic - else Result.ret () + else Result.ret () end hashmap diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index f87ad355..9bfb5070 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -7,12 +7,12 @@ open Primitives namespace hashmap_main -/- [hashmap_main::hashmap::hash_key]: forward function +/- [hashmap_main::hashmap::hash_key]: Source: 'src/hashmap.rs', lines 27:0-27:32 -/ def hashmap.hash_key (k : Usize) : Result Usize := Result.ret k -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0: Source: 'src/hashmap.rs', lines 50:4-56:5 -/ divergent def hashmap.HashMap.allocate_slots_loop (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) : @@ -21,12 +21,12 @@ divergent def hashmap.HashMap.allocate_slots_loop if n > 0#usize then do - let slots0 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil - let n0 ← n - 1#usize - hashmap.HashMap.allocate_slots_loop T slots0 n0 + let v ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil + let n1 ← n - 1#usize + hashmap.HashMap.allocate_slots_loop T v n1 else Result.ret slots -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: Source: 'src/hashmap.rs', lines 50:4-50:76 -/ def hashmap.HashMap.allocate_slots (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) : @@ -34,7 +34,7 @@ def hashmap.HashMap.allocate_slots := hashmap.HashMap.allocate_slots_loop T slots n -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new_with_capacity]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new_with_capacity]: Source: 'src/hashmap.rs', lines 59:4-63:13 -/ def hashmap.HashMap.new_with_capacity (T : Type) (capacity : Usize) (max_load_dividend : Usize) @@ -42,136 +42,106 @@ def hashmap.HashMap.new_with_capacity Result (hashmap.HashMap T) := do - let v := alloc.vec.Vec.new (hashmap.List T) - let slots ← hashmap.HashMap.allocate_slots T v capacity - let i ← capacity * max_load_dividend - let i0 ← i / max_load_divisor - Result.ret - { - num_entries := 0#usize, - max_load_factor := (max_load_dividend, max_load_divisor), - max_load := i0, - slots := slots - } - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new]: forward function + let v := alloc.vec.Vec.new (hashmap.List T) + let slots ← hashmap.HashMap.allocate_slots T v capacity + let i ← capacity * max_load_dividend + let i1 ← i / max_load_divisor + Result.ret + { + num_entries := 0#usize, + max_load_factor := (max_load_dividend, max_load_divisor), + max_load := i1, + slots := slots + } + +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new]: Source: 'src/hashmap.rs', lines 75:4-75:24 -/ def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) := hashmap.HashMap.new_with_capacity T 32#usize 4#usize 5#usize -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: loop 0: Source: 'src/hashmap.rs', lines 80:4-88:5 -/ divergent def hashmap.HashMap.clear_loop (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : Result (alloc.vec.Vec (hashmap.List T)) := - let i0 := alloc.vec.Vec.len (hashmap.List T) slots - if i < i0 + let i1 := alloc.vec.Vec.len (hashmap.List T) slots + if i < i1 then do - let i1 ← i + 1#usize - let slots0 ← - alloc.vec.Vec.index_mut_back (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i - hashmap.List.Nil - hashmap.HashMap.clear_loop T slots0 i1 + let (_, index_mut_back) ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i + let i2 ← i + 1#usize + let slots1 ← index_mut_back hashmap.List.Nil + hashmap.HashMap.clear_loop T slots1 i2 else Result.ret slots -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: Source: 'src/hashmap.rs', lines 80:4-80:27 -/ def hashmap.HashMap.clear (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do - let v ← hashmap.HashMap.clear_loop T self.slots 0#usize - Result.ret { self with num_entries := 0#usize, slots := v } + let back ← hashmap.HashMap.clear_loop T self.slots 0#usize + Result.ret { self with num_entries := 0#usize, slots := back } -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]: Source: 'src/hashmap.rs', lines 90:4-90:30 -/ def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize := Result.ret self.num_entries -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0: Source: 'src/hashmap.rs', lines 97:4-114:5 -/ divergent def hashmap.HashMap.insert_in_list_loop - (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := - match ls with - | hashmap.List.Cons ckey cvalue tl => - if ckey = key - then Result.ret false - else hashmap.HashMap.insert_in_list_loop T key value tl - | hashmap.List.Nil => Result.ret true - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: forward function - Source: 'src/hashmap.rs', lines 97:4-97:71 -/ -def hashmap.HashMap.insert_in_list - (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : Result Bool := - hashmap.HashMap.insert_in_list_loop T key value ls - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0: backward function 0 - Source: 'src/hashmap.rs', lines 97:4-114:5 -/ -divergent def hashmap.HashMap.insert_in_list_loop_back (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : - Result (hashmap.List T) + Result (Bool × (hashmap.List T)) := match ls with | hashmap.List.Cons ckey cvalue tl => if ckey = key - then Result.ret (hashmap.List.Cons ckey value tl) + then Result.ret (false, hashmap.List.Cons ckey value tl) else do - let tl0 ← hashmap.HashMap.insert_in_list_loop_back T key value tl - Result.ret (hashmap.List.Cons ckey cvalue tl0) + let (b, back) ← hashmap.HashMap.insert_in_list_loop T key value tl + Result.ret (b, hashmap.List.Cons ckey cvalue back) | hashmap.List.Nil => let l := hashmap.List.Nil - Result.ret (hashmap.List.Cons key value l) + Result.ret (true, hashmap.List.Cons key value l) -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: backward function 0 +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: Source: 'src/hashmap.rs', lines 97:4-97:71 -/ -def hashmap.HashMap.insert_in_list_back +def hashmap.HashMap.insert_in_list (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : - Result (hashmap.List T) + Result (Bool × (hashmap.List T)) := - hashmap.HashMap.insert_in_list_loop_back T key value ls + hashmap.HashMap.insert_in_list_loop T key value ls -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_no_resize]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_no_resize]: Source: 'src/hashmap.rs', lines 117:4-117:54 -/ def hashmap.HashMap.insert_no_resize (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : Result (hashmap.HashMap T) := do - let hash ← hashmap.hash_key key - let i := alloc.vec.Vec.len (hashmap.List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod - let inserted ← hashmap.HashMap.insert_in_list T key value l - if inserted - then - do - let i0 ← self.num_entries + 1#usize - let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← - alloc.vec.Vec.index_mut_back (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod l0 - Result.ret { self with num_entries := i0, slots := v } - else - do - let l0 ← hashmap.HashMap.insert_in_list_back T key value l - let v ← - alloc.vec.Vec.index_mut_back (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod l0 - Result.ret { self with slots := v } - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) + let hash ← hashmap.hash_key key + let i := alloc.vec.Vec.len (hashmap.List T) self.slots + let hash_mod ← hash % i + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots + hash_mod + let (inserted, l1) ← hashmap.HashMap.insert_in_list T key value l + if inserted + then + do + let i1 ← self.num_entries + 1#usize + let v ← index_mut_back l1 + Result.ret { self with num_entries := i1, slots := v } + else do + let v ← index_mut_back l1 + Result.ret { self with slots := v } + +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0: Source: 'src/hashmap.rs', lines 183:4-196:5 -/ divergent def hashmap.HashMap.move_elements_from_list_loop (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : @@ -180,12 +150,11 @@ divergent def hashmap.HashMap.move_elements_from_list_loop match ls with | hashmap.List.Cons k v tl => do - let ntable0 ← hashmap.HashMap.insert_no_resize T ntable k v - hashmap.HashMap.move_elements_from_list_loop T ntable0 tl + let hm ← hashmap.HashMap.insert_no_resize T ntable k v + hashmap.HashMap.move_elements_from_list_loop T hm tl | hashmap.List.Nil => Result.ret ntable -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: Source: 'src/hashmap.rs', lines 183:4-183:72 -/ def hashmap.HashMap.move_elements_from_list (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : @@ -193,114 +162,111 @@ def hashmap.HashMap.move_elements_from_list := hashmap.HashMap.move_elements_from_list_loop T ntable ls -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: loop 0: Source: 'src/hashmap.rs', lines 171:4-180:5 -/ divergent def hashmap.HashMap.move_elements_loop (T : Type) (ntable : hashmap.HashMap T) (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T))) := - let i0 := alloc.vec.Vec.len (hashmap.List T) slots - if i < i0 + let i1 := alloc.vec.Vec.len (hashmap.List T) slots + if i < i1 then do - let l ← - alloc.vec.Vec.index_mut (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i - let ls := core.mem.replace (hashmap.List T) l hashmap.List.Nil - let ntable0 ← hashmap.HashMap.move_elements_from_list T ntable ls - let i1 ← i + 1#usize - let l0 := core.mem.replace_back (hashmap.List T) l hashmap.List.Nil - let slots0 ← - alloc.vec.Vec.index_mut_back (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i - l0 - hashmap.HashMap.move_elements_loop T ntable0 slots0 i1 + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i + let (ls, l1) := core.mem.replace (hashmap.List T) l hashmap.List.Nil + let hm ← hashmap.HashMap.move_elements_from_list T ntable ls + let i2 ← i + 1#usize + let slots1 ← index_mut_back l1 + let back_'a ← hashmap.HashMap.move_elements_loop T hm slots1 i2 + let (hm1, v) := back_'a + Result.ret (hm1, v) else Result.ret (ntable, slots) -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: Source: 'src/hashmap.rs', lines 171:4-171:95 -/ def hashmap.HashMap.move_elements (T : Type) (ntable : hashmap.HashMap T) (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) : Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T))) := - hashmap.HashMap.move_elements_loop T ntable slots i + do + let back_'a ← hashmap.HashMap.move_elements_loop T ntable slots i + let (hm, v) := back_'a + Result.ret (hm, v) -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]: Source: 'src/hashmap.rs', lines 140:4-140:28 -/ def hashmap.HashMap.try_resize (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := do - let max_usize ← Scalar.cast .Usize core_u32_max - let capacity := alloc.vec.Vec.len (hashmap.List T) self.slots - let n1 ← max_usize / 2#usize - let (i, i0) := self.max_load_factor - let i1 ← n1 / i - if capacity <= i1 - then - do - let i2 ← capacity * 2#usize - let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0 - let (ntable0, _) ← - hashmap.HashMap.move_elements T ntable self.slots 0#usize - Result.ret - { - ntable0 - with - num_entries := self.num_entries, max_load_factor := (i, i0) - } - else Result.ret { self with max_load_factor := (i, i0) } - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) + let max_usize ← Scalar.cast .Usize core_u32_max + let capacity := alloc.vec.Vec.len (hashmap.List T) self.slots + let n1 ← max_usize / 2#usize + let (i, i1) := self.max_load_factor + let i2 ← n1 / i + if capacity <= i2 + then + do + let i3 ← capacity * 2#usize + let ntable ← hashmap.HashMap.new_with_capacity T i3 i i1 + let p ← hashmap.HashMap.move_elements T ntable self.slots 0#usize + let (ntable1, _) := p + Result.ret + { + ntable1 + with + num_entries := self.num_entries, max_load_factor := (i, i1) + } + else Result.ret { self with max_load_factor := (i, i1) } + +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]: Source: 'src/hashmap.rs', lines 129:4-129:48 -/ def hashmap.HashMap.insert (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : Result (hashmap.HashMap T) := do - let self0 ← hashmap.HashMap.insert_no_resize T self key value - let i ← hashmap.HashMap.len T self0 - if i > self0.max_load - then hashmap.HashMap.try_resize T self0 - else Result.ret self0 + let hm ← hashmap.HashMap.insert_no_resize T self key value + let i ← hashmap.HashMap.len T hm + if i > hm.max_load + then hashmap.HashMap.try_resize T hm + else Result.ret hm -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0: Source: 'src/hashmap.rs', lines 206:4-219:5 -/ divergent def hashmap.HashMap.contains_key_in_list_loop (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := match ls with - | hashmap.List.Cons ckey t tl => + | hashmap.List.Cons ckey _ tl => if ckey = key then Result.ret true else hashmap.HashMap.contains_key_in_list_loop T key tl | hashmap.List.Nil => Result.ret false -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: Source: 'src/hashmap.rs', lines 206:4-206:68 -/ def hashmap.HashMap.contains_key_in_list (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool := hashmap.HashMap.contains_key_in_list_loop T key ls -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key]: Source: 'src/hashmap.rs', lines 199:4-199:49 -/ def hashmap.HashMap.contains_key (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool := do - let hash ← hashmap.hash_key key - let i := alloc.vec.Vec.len (hashmap.List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod - hashmap.HashMap.contains_key_in_list T key l - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: loop 0: forward function + let hash ← hashmap.hash_key key + let i := alloc.vec.Vec.len (hashmap.List T) self.slots + let hash_mod ← hash % i + let l ← + alloc.vec.Vec.index (hashmap.List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots + hash_mod + hashmap.HashMap.contains_key_in_list T key l + +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: loop 0: Source: 'src/hashmap.rs', lines 224:4-237:5 -/ divergent def hashmap.HashMap.get_in_list_loop (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := @@ -311,259 +277,194 @@ divergent def hashmap.HashMap.get_in_list_loop else hashmap.HashMap.get_in_list_loop T key tl | hashmap.List.Nil => Result.fail .panic -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: Source: 'src/hashmap.rs', lines 224:4-224:70 -/ def hashmap.HashMap.get_in_list (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := hashmap.HashMap.get_in_list_loop T key ls -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get]: Source: 'src/hashmap.rs', lines 239:4-239:55 -/ def hashmap.HashMap.get (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do - let hash ← hashmap.hash_key key - let i := alloc.vec.Vec.len (hashmap.List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod - hashmap.HashMap.get_in_list T key l - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: forward function + let hash ← hashmap.hash_key key + let i := alloc.vec.Vec.len (hashmap.List T) self.slots + let hash_mod ← hash % i + let l ← + alloc.vec.Vec.index (hashmap.List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots + hash_mod + hashmap.HashMap.get_in_list T key l + +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: Source: 'src/hashmap.rs', lines 245:4-254:5 -/ divergent def hashmap.HashMap.get_mut_in_list_loop - (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := - match ls with - | hashmap.List.Cons ckey cvalue tl => - if ckey = key - then Result.ret cvalue - else hashmap.HashMap.get_mut_in_list_loop T tl key - | hashmap.List.Nil => Result.fail .panic - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: forward function - Source: 'src/hashmap.rs', lines 245:4-245:86 -/ -def hashmap.HashMap.get_mut_in_list - (T : Type) (ls : hashmap.List T) (key : Usize) : Result T := - hashmap.HashMap.get_mut_in_list_loop T ls key - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0 - Source: 'src/hashmap.rs', lines 245:4-254:5 -/ -divergent def hashmap.HashMap.get_mut_in_list_loop_back - (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) : - Result (hashmap.List T) + (T : Type) (ls : hashmap.List T) (key : Usize) : + Result (T × (T → Result (hashmap.List T))) := match ls with | hashmap.List.Cons ckey cvalue tl => if ckey = key - then Result.ret (hashmap.List.Cons ckey ret tl) + then + let back_'a := fun ret => Result.ret (hashmap.List.Cons ckey ret tl) + Result.ret (cvalue, back_'a) else do - let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret - Result.ret (hashmap.List.Cons ckey cvalue tl0) + let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T tl key + let back_'a1 := + fun ret => + do + let tl1 ← back_'a ret + Result.ret (hashmap.List.Cons ckey cvalue tl1) + Result.ret (t, back_'a1) | hashmap.List.Nil => Result.fail .panic -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: backward function 0 +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: Source: 'src/hashmap.rs', lines 245:4-245:86 -/ -def hashmap.HashMap.get_mut_in_list_back - (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) : - Result (hashmap.List T) +def hashmap.HashMap.get_mut_in_list + (T : Type) (ls : hashmap.List T) (key : Usize) : + Result (T × (T → Result (hashmap.List T))) := - hashmap.HashMap.get_mut_in_list_loop_back T ls key ret - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: forward function - Source: 'src/hashmap.rs', lines 257:4-257:67 -/ -def hashmap.HashMap.get_mut - (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T := do - let hash ← hashmap.hash_key key - let i := alloc.vec.Vec.len (hashmap.List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod - hashmap.HashMap.get_mut_in_list T l key + let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key + let back_'a1 := fun ret => back_'a ret + Result.ret (t, back_'a1) -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: backward function 0 +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: Source: 'src/hashmap.rs', lines 257:4-257:67 -/ -def hashmap.HashMap.get_mut_back - (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret : T) : - Result (hashmap.HashMap T) +def hashmap.HashMap.get_mut + (T : Type) (self : hashmap.HashMap T) (key : Usize) : + Result (T × (T → Result (hashmap.HashMap T))) := do - let hash ← hashmap.hash_key key - let i := alloc.vec.Vec.len (hashmap.List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod - let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret - let v ← - alloc.vec.Vec.index_mut_back (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod l0 - Result.ret { self with slots := v } - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: forward function - Source: 'src/hashmap.rs', lines 265:4-291:5 -/ -divergent def hashmap.HashMap.remove_from_list_loop - (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := - match ls with - | hashmap.List.Cons ckey t tl => - if ckey = key - then - let mv_ls := - core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) - hashmap.List.Nil - match mv_ls with - | hashmap.List.Cons i cvalue tl0 => Result.ret (some cvalue) - | hashmap.List.Nil => Result.fail .panic - else hashmap.HashMap.remove_from_list_loop T key tl - | hashmap.List.Nil => Result.ret none - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: forward function - Source: 'src/hashmap.rs', lines 265:4-265:69 -/ -def hashmap.HashMap.remove_from_list - (T : Type) (key : Usize) (ls : hashmap.List T) : Result (Option T) := - hashmap.HashMap.remove_from_list_loop T key ls + let hash ← hashmap.hash_key key + let i := alloc.vec.Vec.len (hashmap.List T) self.slots + let hash_mod ← hash % i + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots + hash_mod + let (t, get_mut_in_list_back) ← hashmap.HashMap.get_mut_in_list T l key + let back_'a := + fun ret => + do + let l1 ← get_mut_in_list_back ret + let v ← index_mut_back l1 + Result.ret { self with slots := v } + Result.ret (t, back_'a) -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: backward function 1 +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0: Source: 'src/hashmap.rs', lines 265:4-291:5 -/ -divergent def hashmap.HashMap.remove_from_list_loop_back - (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := +divergent def hashmap.HashMap.remove_from_list_loop + (T : Type) (key : Usize) (ls : hashmap.List T) : + Result ((Option T) × (hashmap.List T)) + := match ls with | hashmap.List.Cons ckey t tl => if ckey = key then - let mv_ls := + let (mv_ls, _) := core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) hashmap.List.Nil match mv_ls with - | hashmap.List.Cons i cvalue tl0 => Result.ret tl0 + | hashmap.List.Cons _ cvalue tl1 => Result.ret (some cvalue, tl1) | hashmap.List.Nil => Result.fail .panic else do - let tl0 ← hashmap.HashMap.remove_from_list_loop_back T key tl - Result.ret (hashmap.List.Cons ckey t tl0) - | hashmap.List.Nil => Result.ret hashmap.List.Nil + let (o, back) ← hashmap.HashMap.remove_from_list_loop T key tl + Result.ret (o, hashmap.List.Cons ckey t back) + | hashmap.List.Nil => Result.ret (none, hashmap.List.Nil) -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: backward function 1 +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: Source: 'src/hashmap.rs', lines 265:4-265:69 -/ -def hashmap.HashMap.remove_from_list_back - (T : Type) (key : Usize) (ls : hashmap.List T) : Result (hashmap.List T) := - hashmap.HashMap.remove_from_list_loop_back T key ls +def hashmap.HashMap.remove_from_list + (T : Type) (key : Usize) (ls : hashmap.List T) : + Result ((Option T) × (hashmap.List T)) + := + hashmap.HashMap.remove_from_list_loop T key ls -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove]: forward function +/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove]: Source: 'src/hashmap.rs', lines 294:4-294:52 -/ def hashmap.HashMap.remove - (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) := - do - let hash ← hashmap.hash_key key - let i := alloc.vec.Vec.len (hashmap.List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod - let x ← hashmap.HashMap.remove_from_list T key l - match x with - | none => Result.ret none - | some x0 => do - let _ ← self.num_entries - 1#usize - Result.ret (some x0) - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove]: backward function 0 - Source: 'src/hashmap.rs', lines 294:4-294:52 -/ -def hashmap.HashMap.remove_back (T : Type) (self : hashmap.HashMap T) (key : Usize) : - Result (hashmap.HashMap T) + Result ((Option T) × (hashmap.HashMap T)) := do - let hash ← hashmap.hash_key key - let i := alloc.vec.Vec.len (hashmap.List T) self.slots - let hash_mod ← hash % i - let l ← - alloc.vec.Vec.index_mut (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod - let x ← hashmap.HashMap.remove_from_list T key l - match x with - | none => - do - let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← - alloc.vec.Vec.index_mut_back (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod l0 - Result.ret { self with slots := v } - | some x0 => - do - let i0 ← self.num_entries - 1#usize - let l0 ← hashmap.HashMap.remove_from_list_back T key l - let v ← - alloc.vec.Vec.index_mut_back (hashmap.List T) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) - self.slots hash_mod l0 - Result.ret { self with num_entries := i0, slots := v } - -/- [hashmap_main::hashmap::test1]: forward function + let hash ← hashmap.hash_key key + let i := alloc.vec.Vec.len (hashmap.List T) self.slots + let hash_mod ← hash % i + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (hashmap.List T) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots + hash_mod + let (x, l1) ← hashmap.HashMap.remove_from_list T key l + match x with + | none => + do + let v ← index_mut_back l1 + Result.ret (none, { self with slots := v }) + | some x1 => + do + let i1 ← self.num_entries - 1#usize + let v ← index_mut_back l1 + Result.ret (some x1, { self with num_entries := i1, slots := v }) + +/- [hashmap_main::hashmap::test1]: Source: 'src/hashmap.rs', lines 315:0-315:10 -/ def hashmap.test1 : Result Unit := do - let hm ← hashmap.HashMap.new U64 - let hm0 ← hashmap.HashMap.insert U64 hm 0#usize 42#u64 - let hm1 ← hashmap.HashMap.insert U64 hm0 128#usize 18#u64 - let hm2 ← hashmap.HashMap.insert U64 hm1 1024#usize 138#u64 - let hm3 ← hashmap.HashMap.insert U64 hm2 1056#usize 256#u64 - let i ← hashmap.HashMap.get U64 hm3 128#usize - if not (i = 18#u64) + let hm ← hashmap.HashMap.new U64 + let hm1 ← hashmap.HashMap.insert U64 hm 0#usize 42#u64 + let hm2 ← hashmap.HashMap.insert U64 hm1 128#usize 18#u64 + let hm3 ← hashmap.HashMap.insert U64 hm2 1024#usize 138#u64 + let hm4 ← hashmap.HashMap.insert U64 hm3 1056#usize 256#u64 + let i ← hashmap.HashMap.get U64 hm4 128#usize + if not (i = 18#u64) + then Result.fail .panic + else + do + let (_, get_mut_back) ← hashmap.HashMap.get_mut U64 hm4 1024#usize + let hm5 ← get_mut_back 56#u64 + let i1 ← hashmap.HashMap.get U64 hm5 1024#usize + if not (i1 = 56#u64) then Result.fail .panic else do - let hm4 ← hashmap.HashMap.get_mut_back U64 hm3 1024#usize 56#u64 - let i0 ← hashmap.HashMap.get U64 hm4 1024#usize - if not (i0 = 56#u64) + let (x, hm6) ← hashmap.HashMap.remove U64 hm5 1024#usize + match x with + | none => Result.fail .panic + | some x1 => + if not (x1 = 56#u64) then Result.fail .panic else do - let x ← hashmap.HashMap.remove U64 hm4 1024#usize - match x with - | none => Result.fail .panic - | some x0 => - if not (x0 = 56#u64) + let i2 ← hashmap.HashMap.get U64 hm6 0#usize + if not (i2 = 42#u64) + then Result.fail .panic + else + do + let i3 ← hashmap.HashMap.get U64 hm6 128#usize + if not (i3 = 18#u64) + then Result.fail .panic + else + do + let i4 ← hashmap.HashMap.get U64 hm6 1056#usize + if not (i4 = 256#u64) then Result.fail .panic - else - do - let hm5 ← hashmap.HashMap.remove_back U64 hm4 1024#usize - let i1 ← hashmap.HashMap.get U64 hm5 0#usize - if not (i1 = 42#u64) - then Result.fail .panic - else - do - let i2 ← hashmap.HashMap.get U64 hm5 128#usize - if not (i2 = 18#u64) - then Result.fail .panic - else - do - let i3 ← hashmap.HashMap.get U64 hm5 1056#usize - if not (i3 = 256#u64) - then Result.fail .panic - else Result.ret () - -/- [hashmap_main::insert_on_disk]: forward function + else Result.ret () + +/- [hashmap_main::insert_on_disk]: Source: 'src/hashmap_main.rs', lines 7:0-7:43 -/ def insert_on_disk (key : Usize) (value : U64) (st : State) : Result (State × Unit) := do - let (st0, hm) ← hashmap_utils.deserialize st - let hm0 ← hashmap.HashMap.insert U64 hm key value - let (st1, _) ← hashmap_utils.serialize hm0 st0 - Result.ret (st1, ()) + let (st1, hm) ← hashmap_utils.deserialize st + let hm1 ← hashmap.HashMap.insert U64 hm key value + let (st2, _) ← hashmap_utils.serialize hm1 st1 + Result.ret (st2, ()) -/- [hashmap_main::main]: forward function +/- [hashmap_main::main]: Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/ def main : Result Unit := Result.ret () diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean index 02ca5b0e..c09edbd2 100644 --- a/tests/lean/HashmapMain/FunsExternal_Template.lean +++ b/tests/lean/HashmapMain/FunsExternal_Template.lean @@ -6,12 +6,12 @@ import HashmapMain.Types open Primitives open hashmap_main -/- [hashmap_main::hashmap_utils::deserialize]: forward function +/- [hashmap_main::hashmap_utils::deserialize]: Source: 'src/hashmap_utils.rs', lines 10:0-10:43 -/ axiom hashmap_utils.deserialize : State → Result (State × (hashmap.HashMap U64)) -/- [hashmap_main::hashmap_utils::serialize]: forward function +/- [hashmap_main::hashmap_utils::serialize]: Source: 'src/hashmap_utils.rs', lines 5:0-5:42 -/ axiom hashmap_utils.serialize : hashmap.HashMap U64 → State → Result (State × Unit) diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 08aa08a5..805ecabc 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -5,73 +5,72 @@ open Primitives namespace loops -/- [loops::sum]: loop 0: forward function +/- [loops::sum]: loop 0: Source: 'src/loops.rs', lines 4:0-14:1 -/ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max then do - let s0 ← s + i - let i0 ← i + 1#u32 - sum_loop max i0 s0 + let s1 ← s + i + let i1 ← i + 1#u32 + sum_loop max i1 s1 else s * 2#u32 -/- [loops::sum]: forward function +/- [loops::sum]: Source: 'src/loops.rs', lines 4:0-4:27 -/ def sum (max : U32) : Result U32 := sum_loop max 0#u32 0#u32 -/- [loops::sum_with_mut_borrows]: loop 0: forward function +/- [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 -/ divergent def sum_with_mut_borrows_loop (max : U32) (mi : U32) (ms : U32) : Result U32 := if mi < max then do - let ms0 ← ms + mi - let mi0 ← mi + 1#u32 - sum_with_mut_borrows_loop max mi0 ms0 + let ms1 ← ms + mi + let mi1 ← mi + 1#u32 + sum_with_mut_borrows_loop max mi1 ms1 else ms * 2#u32 -/- [loops::sum_with_mut_borrows]: forward function +/- [loops::sum_with_mut_borrows]: Source: 'src/loops.rs', lines 19:0-19:44 -/ def sum_with_mut_borrows (max : U32) : Result U32 := sum_with_mut_borrows_loop max 0#u32 0#u32 -/- [loops::sum_with_shared_borrows]: loop 0: forward function +/- [loops::sum_with_shared_borrows]: loop 0: Source: 'src/loops.rs', lines 34:0-48:1 -/ divergent def sum_with_shared_borrows_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max then do - let i0 ← i + 1#u32 - let s0 ← s + i0 - sum_with_shared_borrows_loop max i0 s0 + let i1 ← i + 1#u32 + let s1 ← s + i1 + sum_with_shared_borrows_loop max i1 s1 else s * 2#u32 -/- [loops::sum_with_shared_borrows]: forward function +/- [loops::sum_with_shared_borrows]: Source: 'src/loops.rs', lines 34:0-34:47 -/ def sum_with_shared_borrows (max : U32) : Result U32 := sum_with_shared_borrows_loop max 0#u32 0#u32 -/- [loops::clear]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [loops::clear]: loop 0: Source: 'src/loops.rs', lines 52:0-58:1 -/ divergent def clear_loop (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) := - let i0 := alloc.vec.Vec.len U32 v - if i < i0 + let i1 := alloc.vec.Vec.len U32 v + if i < i1 then do - let i1 ← i + 1#usize - let v0 ← - alloc.vec.Vec.index_mut_back U32 Usize - (core.slice.index.SliceIndexUsizeSliceTInst U32) v i 0#u32 - clear_loop v0 i1 + let (_, index_mut_back) ← + alloc.vec.Vec.index_mut U32 Usize + (core.slice.index.SliceIndexUsizeSliceTInst U32) v i + let i2 ← i + 1#usize + let v1 ← index_mut_back 0#u32 + clear_loop v1 i2 else Result.ret v -/- [loops::clear]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [loops::clear]: Source: 'src/loops.rs', lines 52:0-52:30 -/ def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := clear_loop v 0#usize @@ -82,7 +81,7 @@ inductive List (T : Type) := | Cons : T → List T → List T | Nil : List T -/- [loops::list_mem]: loop 0: forward function +/- [loops::list_mem]: loop 0: Source: 'src/loops.rs', lines 66:0-75:1 -/ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := match ls with @@ -91,51 +90,42 @@ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := else list_mem_loop x tl | List.Nil => Result.ret false -/- [loops::list_mem]: forward function +/- [loops::list_mem]: Source: 'src/loops.rs', lines 66:0-66:52 -/ def list_mem (x : U32) (ls : List U32) : Result Bool := list_mem_loop x ls -/- [loops::list_nth_mut_loop]: loop 0: forward function +/- [loops::list_nth_mut_loop]: loop 0: Source: 'src/loops.rs', lines 78:0-88:1 -/ 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 = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_loop T tl i0 - | List.Nil => Result.fail .panic - -/- [loops::list_nth_mut_loop]: forward function - Source: 'src/loops.rs', lines 78:0-78:71 -/ -def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T := - list_nth_mut_loop_loop T ls i - -/- [loops::list_nth_mut_loop]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 78:0-88:1 -/ -divergent def list_nth_mut_loop_loop_back - (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) := + (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := match ls with | List.Cons x tl => if i = 0#u32 - then Result.ret (List.Cons ret tl) + then + let back := fun ret => Result.ret (List.Cons ret tl) + Result.ret (x, back) else do - let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret - Result.ret (List.Cons x tl0) + let i1 ← i - 1#u32 + let (t, back) ← list_nth_mut_loop_loop T tl i1 + let back1 := + fun ret => do + let tl1 ← back ret + Result.ret (List.Cons x tl1) + Result.ret (t, back1) | List.Nil => Result.fail .panic -/- [loops::list_nth_mut_loop]: backward function 0 +/- [loops::list_nth_mut_loop]: Source: 'src/loops.rs', lines 78:0-78:71 -/ -def list_nth_mut_loop_back - (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) := - list_nth_mut_loop_loop_back T ls i ret +def list_nth_mut_loop + (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := + do + let (t, back) ← list_nth_mut_loop_loop T ls i + let back1 := fun ret => back ret + Result.ret (t, back1) -/- [loops::list_nth_shared_loop]: loop 0: forward function +/- [loops::list_nth_shared_loop]: loop 0: Source: 'src/loops.rs', lines 91:0-101:1 -/ divergent def list_nth_shared_loop_loop (T : Type) (ls : List T) (i : U32) : Result T := @@ -144,64 +134,54 @@ divergent def list_nth_shared_loop_loop if i = 0#u32 then Result.ret x else do - let i0 ← i - 1#u32 - list_nth_shared_loop_loop T tl i0 + let i1 ← i - 1#u32 + list_nth_shared_loop_loop T tl i1 | List.Nil => Result.fail .panic -/- [loops::list_nth_shared_loop]: forward function +/- [loops::list_nth_shared_loop]: Source: 'src/loops.rs', lines 91:0-91:66 -/ def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T := list_nth_shared_loop_loop T ls i -/- [loops::get_elem_mut]: loop 0: forward function +/- [loops::get_elem_mut]: loop 0: Source: 'src/loops.rs', lines 103:0-117:1 -/ -divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize := - match ls with - | List.Cons y tl => if y = x - then Result.ret y - else get_elem_mut_loop x tl - | List.Nil => Result.fail .panic - -/- [loops::get_elem_mut]: forward function - Source: 'src/loops.rs', lines 103:0-103:73 -/ -def get_elem_mut - (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := - do - let l ← - alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - get_elem_mut_loop x l - -/- [loops::get_elem_mut]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 103:0-117:1 -/ -divergent def get_elem_mut_loop_back - (x : Usize) (ls : List Usize) (ret : Usize) : Result (List Usize) := +divergent def get_elem_mut_loop + (x : Usize) (ls : List Usize) : + Result (Usize × (Usize → Result (List Usize))) + := match ls with | List.Cons y tl => if y = x - then Result.ret (List.Cons ret tl) + then + let back := fun ret => Result.ret (List.Cons ret tl) + Result.ret (y, back) else do - let tl0 ← get_elem_mut_loop_back x tl ret - Result.ret (List.Cons y tl0) + let (i, back) ← get_elem_mut_loop x tl + let back1 := + fun ret => do + let tl1 ← back ret + Result.ret (List.Cons y tl1) + Result.ret (i, back1) | List.Nil => Result.fail .panic -/- [loops::get_elem_mut]: backward function 0 +/- [loops::get_elem_mut]: Source: 'src/loops.rs', lines 103:0-103:73 -/ -def get_elem_mut_back - (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret : Usize) : - Result (alloc.vec.Vec (List Usize)) +def get_elem_mut + (slots : alloc.vec.Vec (List Usize)) (x : Usize) : + Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize)))) := do - let l ← - alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - let l0 ← get_elem_mut_loop_back x l ret - alloc.vec.Vec.index_mut_back (List Usize) Usize + let (l, index_mut_back) ← + alloc.vec.Vec.index_mut (List Usize) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - l0 + let (i, back) ← get_elem_mut_loop x l + let back1 := fun ret => do + let l1 ← back ret + index_mut_back l1 + Result.ret (i, back1) -/- [loops::get_elem_shared]: loop 0: forward function +/- [loops::get_elem_shared]: loop 0: Source: 'src/loops.rs', lines 119:0-133:1 -/ divergent def get_elem_shared_loop (x : Usize) (ls : List Usize) : Result Usize := @@ -211,76 +191,64 @@ divergent def get_elem_shared_loop else get_elem_shared_loop x tl | List.Nil => Result.fail .panic -/- [loops::get_elem_shared]: forward function +/- [loops::get_elem_shared]: Source: 'src/loops.rs', lines 119:0-119:68 -/ def get_elem_shared (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := do - let l ← - alloc.vec.Vec.index (List Usize) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - get_elem_shared_loop x l - -/- [loops::id_mut]: forward function - Source: 'src/loops.rs', lines 135:0-135:50 -/ -def id_mut (T : Type) (ls : List T) : Result (List T) := - Result.ret ls + let l ← + alloc.vec.Vec.index (List Usize) Usize + (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize + get_elem_shared_loop x l -/- [loops::id_mut]: backward function 0 +/- [loops::id_mut]: Source: 'src/loops.rs', lines 135:0-135:50 -/ -def id_mut_back (T : Type) (ls : List T) (ret : List T) : Result (List T) := - Result.ret ret +def id_mut + (T : Type) (ls : List T) : + Result ((List T) × (List T → Result (List T))) + := + let back := fun ret => Result.ret ret + Result.ret (ls, back) -/- [loops::id_shared]: forward function +/- [loops::id_shared]: Source: 'src/loops.rs', lines 139:0-139:45 -/ def id_shared (T : Type) (ls : List T) : Result (List T) := Result.ret ls -/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function +/- [loops::list_nth_mut_loop_with_id]: loop 0: Source: 'src/loops.rs', lines 144:0-155:1 -/ divergent def list_nth_mut_loop_with_id_loop - (T : Type) (i : U32) (ls : List T) : Result T := + (T : Type) (i : U32) (ls : List T) : Result (T × (T → Result (List T))) := match ls with | List.Cons x tl => if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_with_id_loop T i0 tl - | List.Nil => Result.fail .panic - -/- [loops::list_nth_mut_loop_with_id]: forward function - Source: 'src/loops.rs', lines 144:0-144:75 -/ -def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T := - do - let ls0 ← id_mut T ls - list_nth_mut_loop_with_id_loop T i ls0 - -/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 144:0-155:1 -/ -divergent def list_nth_mut_loop_with_id_loop_back - (T : Type) (i : U32) (ls : List T) (ret : T) : Result (List T) := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret (List.Cons ret tl) + then + let back := fun ret => Result.ret (List.Cons ret tl) + Result.ret (x, back) else do - let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret - Result.ret (List.Cons x tl0) + let i1 ← i - 1#u32 + let (t, back) ← list_nth_mut_loop_with_id_loop T i1 tl + let back1 := + fun ret => do + let tl1 ← back ret + Result.ret (List.Cons x tl1) + Result.ret (t, back1) | List.Nil => Result.fail .panic -/- [loops::list_nth_mut_loop_with_id]: backward function 0 +/- [loops::list_nth_mut_loop_with_id]: Source: 'src/loops.rs', lines 144:0-144:75 -/ -def list_nth_mut_loop_with_id_back - (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) := +def list_nth_mut_loop_with_id + (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := do - let ls0 ← id_mut T ls - let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret - id_mut_back T ls l - -/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function + let (ls1, id_mut_back) ← id_mut T ls + let (t, back) ← list_nth_mut_loop_with_id_loop T i ls1 + let back1 := fun ret => do + let l ← back ret + id_mut_back l + Result.ret (t, back1) + +/- [loops::list_nth_shared_loop_with_id]: loop 0: Source: 'src/loops.rs', lines 158:0-169:1 -/ divergent def list_nth_shared_loop_with_id_loop (T : Type) (i : U32) (ls : List T) : Result T := @@ -289,97 +257,62 @@ divergent def list_nth_shared_loop_with_id_loop if i = 0#u32 then Result.ret x else do - let i0 ← i - 1#u32 - list_nth_shared_loop_with_id_loop T i0 tl + let i1 ← i - 1#u32 + list_nth_shared_loop_with_id_loop T i1 tl | List.Nil => Result.fail .panic -/- [loops::list_nth_shared_loop_with_id]: forward function +/- [loops::list_nth_shared_loop_with_id]: Source: 'src/loops.rs', lines 158:0-158:70 -/ def list_nth_shared_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T := do - let ls0 ← id_shared T ls - list_nth_shared_loop_with_id_loop T i ls0 + let ls1 ← id_shared T ls + list_nth_shared_loop_with_id_loop T i ls1 -/- [loops::list_nth_mut_loop_pair]: loop 0: forward function +/- [loops::list_nth_mut_loop_pair]: loop 0: Source: 'src/loops.rs', lines 174:0-195:1 -/ divergent def list_nth_mut_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail .panic - | List.Nil => Result.fail .panic - -/- [loops::list_nth_mut_loop_pair]: forward function - Source: 'src/loops.rs', lines 174:0-178:27 -/ -def list_nth_mut_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 174:0-195:1 -/ -divergent def list_nth_mut_loop_pair_loop_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T)) × (T → Result (List T))) := match ls0 with | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret tl0) + then + let back_'a := fun ret => Result.ret (List.Cons ret tl0) + let back_'b := fun ret => Result.ret (List.Cons ret tl1) + Result.ret ((x0, x1), back_'a, back_'b) else do - let i0 ← i - 1#u32 - let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret - Result.ret (List.Cons x0 tl00) + let i1 ← i - 1#u32 + let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1 + let back_'a1 := + fun ret => do + let tl01 ← back_'a ret + Result.ret (List.Cons x0 tl01) + let back_'b1 := + fun ret => do + let tl11 ← back_'b ret + Result.ret (List.Cons x1 tl11) + Result.ret (p, back_'a1, back_'b1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_mut_loop_pair]: backward function 0 +/- [loops::list_nth_mut_loop_pair]: Source: 'src/loops.rs', lines 174:0-178:27 -/ -def list_nth_mut_loop_pair_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) - := - list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret - -/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 - Source: 'src/loops.rs', lines 174:0-195:1 -/ -divergent def list_nth_mut_loop_pair_loop_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret tl1) - else - do - let i0 ← i - 1#u32 - let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret - Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail .panic - | List.Nil => Result.fail .panic - -/- [loops::list_nth_mut_loop_pair]: backward function 1 - Source: 'src/loops.rs', lines 174:0-178:27 -/ -def list_nth_mut_loop_pair_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) +def list_nth_mut_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T)) × (T → Result (List T))) := - list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret + do + let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i + let back_'a1 := fun ret => back_'a ret + let back_'b1 := fun ret => back_'b ret + Result.ret (p, back_'a1, back_'b1) -/- [loops::list_nth_shared_loop_pair]: loop 0: forward function +/- [loops::list_nth_shared_loop_pair]: loop 0: Source: 'src/loops.rs', lines 198:0-219:1 -/ divergent def list_nth_shared_loop_pair_loop (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := @@ -390,71 +323,59 @@ divergent def list_nth_shared_loop_pair_loop if i = 0#u32 then Result.ret (x0, x1) else do - let i0 ← i - 1#u32 - list_nth_shared_loop_pair_loop T tl0 tl1 i0 + let i1 ← i - 1#u32 + list_nth_shared_loop_pair_loop T tl0 tl1 i1 | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_shared_loop_pair]: forward function +/- [loops::list_nth_shared_loop_pair]: Source: 'src/loops.rs', lines 198:0-202:19 -/ def list_nth_shared_loop_pair (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_loop_pair_loop T ls0 ls1 i -/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function +/- [loops::list_nth_mut_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 223:0-238:1 -/ divergent def list_nth_mut_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail .panic - | List.Nil => Result.fail .panic - -/- [loops::list_nth_mut_loop_pair_merge]: forward function - Source: 'src/loops.rs', lines 223:0-227:27 -/ -def list_nth_mut_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 223:0-238:1 -/ -divergent def list_nth_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) : - Result ((List T) × (List T)) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × ((T × T) → Result ((List T) × (List T)))) := match ls0 with | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then let (t, t0) := ret - Result.ret (List.Cons t tl0, List.Cons t0 tl1) + then + let back_'a := + fun ret => + let (t, t1) := ret + Result.ret (List.Cons t tl0, List.Cons t1 tl1) + Result.ret ((x0, x1), back_'a) else do - let i0 ← i - 1#u32 - let (tl00, tl10) ← - list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret - Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) + let i1 ← i - 1#u32 + let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1 + let back_'a1 := + fun ret => + do + let (tl01, tl11) ← back_'a ret + Result.ret (List.Cons x0 tl01, List.Cons x1 tl11) + Result.ret (p, back_'a1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 +/- [loops::list_nth_mut_loop_pair_merge]: Source: 'src/loops.rs', lines 223:0-227:27 -/ -def list_nth_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) : - Result ((List T) × (List T)) +def list_nth_mut_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × ((T × T) → Result ((List T) × (List T)))) := - list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret + do + let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i + let back_'a1 := fun ret => back_'a ret + Result.ret (p, back_'a1) -/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function +/- [loops::list_nth_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 241:0-256:1 -/ divergent def list_nth_shared_loop_pair_merge_loop (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := @@ -466,221 +387,165 @@ divergent def list_nth_shared_loop_pair_merge_loop then Result.ret (x0, x1) else do - let i0 ← i - 1#u32 - list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0 + let i1 ← i - 1#u32 + list_nth_shared_loop_pair_merge_loop T tl0 tl1 i1 | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_shared_loop_pair_merge]: forward function +/- [loops::list_nth_shared_loop_pair_merge]: Source: 'src/loops.rs', lines 241:0-245:19 -/ def list_nth_shared_loop_pair_merge (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := list_nth_shared_loop_pair_merge_loop T ls0 ls1 i -/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function +/- [loops::list_nth_mut_shared_loop_pair]: loop 0: Source: 'src/loops.rs', lines 259:0-274:1 -/ divergent def list_nth_mut_shared_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail .panic - | List.Nil => Result.fail .panic - -/- [loops::list_nth_mut_shared_loop_pair]: forward function - Source: 'src/loops.rs', lines 259:0-263:23 -/ -def list_nth_mut_shared_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_shared_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 259:0-274:1 -/ -divergent def list_nth_mut_shared_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := match ls0 with | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret tl0) + then + let back_'a := fun ret => Result.ret (List.Cons ret tl0) + Result.ret ((x0, x1), back_'a) else do - let i0 ← i - 1#u32 - let tl00 ← list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret - Result.ret (List.Cons x0 tl00) + let i1 ← i - 1#u32 + let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1 + let back_'a1 := + fun ret => do + let tl01 ← back_'a ret + Result.ret (List.Cons x0 tl01) + Result.ret (p, back_'a1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 +/- [loops::list_nth_mut_shared_loop_pair]: Source: 'src/loops.rs', lines 259:0-263:23 -/ -def list_nth_mut_shared_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) +def list_nth_mut_shared_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := - list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret + do + let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i + let back_'a1 := fun ret => back_'a ret + Result.ret (p, back_'a1) -/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function +/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 278:0-293:1 -/ divergent def list_nth_mut_shared_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail .panic - | List.Nil => Result.fail .panic - -/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function - Source: 'src/loops.rs', lines 278:0-282:23 -/ -def list_nth_mut_shared_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 278:0-293:1 -/ -divergent def list_nth_mut_shared_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := match ls0 with | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret tl0) + then + let back_'a := fun ret => Result.ret (List.Cons ret tl0) + Result.ret ((x0, x1), back_'a) else do - let i0 ← i - 1#u32 - let tl00 ← - list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret - Result.ret (List.Cons x0 tl00) + let i1 ← i - 1#u32 + let (p, back_'a) ← + list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1 + let back_'a1 := + fun ret => do + let tl01 ← back_'a ret + Result.ret (List.Cons x0 tl01) + Result.ret (p, back_'a1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 +/- [loops::list_nth_mut_shared_loop_pair_merge]: Source: 'src/loops.rs', lines 278:0-282:23 -/ -def list_nth_mut_shared_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) +def list_nth_mut_shared_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := - list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret + do + let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i + let back_'a1 := fun ret => back_'a ret + Result.ret (p, back_'a1) -/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function +/- [loops::list_nth_shared_mut_loop_pair]: loop 0: Source: 'src/loops.rs', lines 297:0-312:1 -/ divergent def list_nth_shared_mut_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail .panic - | List.Nil => Result.fail .panic - -/- [loops::list_nth_shared_mut_loop_pair]: forward function - Source: 'src/loops.rs', lines 297:0-301:23 -/ -def list_nth_shared_mut_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_mut_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 - Source: 'src/loops.rs', lines 297:0-312:1 -/ -divergent def list_nth_shared_mut_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := match ls0 with | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret tl1) + then + let back_'b := fun ret => Result.ret (List.Cons ret tl1) + Result.ret ((x0, x1), back_'b) else do - let i0 ← i - 1#u32 - let tl10 ← list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret - Result.ret (List.Cons x1 tl10) + let i1 ← i - 1#u32 + let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1 + let back_'b1 := + fun ret => do + let tl11 ← back_'b ret + Result.ret (List.Cons x1 tl11) + Result.ret (p, back_'b1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 +/- [loops::list_nth_shared_mut_loop_pair]: Source: 'src/loops.rs', lines 297:0-301:23 -/ -def list_nth_shared_mut_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) +def list_nth_shared_mut_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := - list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret + do + let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i + let back_'b1 := fun ret => back_'b ret + Result.ret (p, back_'b1) -/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function +/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: Source: 'src/loops.rs', lines 316:0-331:1 -/ divergent def list_nth_shared_mut_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail .panic - | List.Nil => Result.fail .panic - -/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function - Source: 'src/loops.rs', lines 316:0-320:23 -/ -def list_nth_shared_mut_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 - Source: 'src/loops.rs', lines 316:0-331:1 -/ -divergent def list_nth_shared_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := match ls0 with | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret tl1) + then + let back_'a := fun ret => Result.ret (List.Cons ret tl1) + Result.ret ((x0, x1), back_'a) else do - let i0 ← i - 1#u32 - let tl10 ← - list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret - Result.ret (List.Cons x1 tl10) + let i1 ← i - 1#u32 + let (p, back_'a) ← + list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1 + let back_'a1 := + fun ret => do + let tl11 ← back_'a ret + Result.ret (List.Cons x1 tl11) + Result.ret (p, back_'a1) | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic -/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 +/- [loops::list_nth_shared_mut_loop_pair_merge]: Source: 'src/loops.rs', lines 316:0-320:23 -/ -def list_nth_shared_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : - Result (List T) +def list_nth_shared_mut_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : + Result ((T × T) × (T → Result (List T))) := - list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret + do + let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i + let back_'a1 := fun ret => back_'a ret + Result.ret (p, back_'a1) end loops diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 08386bb7..015fec84 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -5,55 +5,51 @@ open Primitives namespace paper -/- [paper::ref_incr]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [paper::ref_incr]: Source: 'src/paper.rs', lines 4:0-4:28 -/ def ref_incr (x : I32) : Result I32 := x + 1#i32 -/- [paper::test_incr]: forward function +/- [paper::test_incr]: Source: 'src/paper.rs', lines 8:0-8:18 -/ def test_incr : Result Unit := do - let x ← ref_incr 0#i32 - if not (x = 1#i32) - then Result.fail .panic - else Result.ret () + let i ← ref_incr 0#i32 + if not (i = 1#i32) + then Result.fail .panic + else Result.ret () /- Unit test for [paper::test_incr] -/ #assert (test_incr == Result.ret ()) -/- [paper::choose]: forward function - Source: 'src/paper.rs', lines 15:0-15:70 -/ -def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T := - if b - then Result.ret x - else Result.ret y - -/- [paper::choose]: backward function 0 +/- [paper::choose]: Source: 'src/paper.rs', lines 15:0-15:70 -/ -def choose_back - (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) := +def choose + (T : Type) (b : Bool) (x : T) (y : T) : + Result (T × (T → Result (T × T))) + := if b - then Result.ret (ret, y) - else Result.ret (x, ret) + then let back_'a := fun ret => Result.ret (ret, y) + Result.ret (x, back_'a) + else let back_'a := fun ret => Result.ret (x, ret) + Result.ret (y, back_'a) -/- [paper::test_choose]: forward function +/- [paper::test_choose]: Source: 'src/paper.rs', lines 23:0-23:20 -/ def test_choose : Result Unit := do - let z ← choose I32 true 0#i32 0#i32 - let z0 ← z + 1#i32 - if not (z0 = 1#i32) + let (z, choose_back) ← choose I32 true 0#i32 0#i32 + let z1 ← z + 1#i32 + if not (z1 = 1#i32) + then Result.fail .panic + else + do + let (x, y) ← choose_back z1 + if not (x = 1#i32) then Result.fail .panic - else - do - let (x, y) ← choose_back I32 true 0#i32 0#i32 z0 - if not (x = 1#i32) - then Result.fail .panic - else if not (y = 0#i32) - then Result.fail .panic - else Result.ret () + else if not (y = 0#i32) + then Result.fail .panic + else Result.ret () /- Unit test for [paper::test_choose] -/ #assert (test_choose == Result.ret ()) @@ -64,68 +60,63 @@ inductive List (T : Type) := | Cons : T → List T → List T | Nil : List T -/- [paper::list_nth_mut]: forward function +/- [paper::list_nth_mut]: Source: 'src/paper.rs', lines 42:0-42:67 -/ -divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T := +divergent def list_nth_mut + (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with | List.Cons x tl => if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_mut T tl i0 - | List.Nil => Result.fail .panic - -/- [paper::list_nth_mut]: backward function 0 - Source: 'src/paper.rs', lines 42:0-42:67 -/ -divergent def list_nth_mut_back - (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) := - match l with - | List.Cons x tl => - if i = 0#u32 - then Result.ret (List.Cons ret tl) + then + let back_'a := fun ret => Result.ret (List.Cons ret tl) + Result.ret (x, back_'a) else do - let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_back T tl i0 ret - Result.ret (List.Cons x tl0) + let i1 ← i - 1#u32 + let (t, list_nth_mut_back) ← list_nth_mut T tl i1 + let back_'a := + fun ret => + do + let tl1 ← list_nth_mut_back ret + Result.ret (List.Cons x tl1) + Result.ret (t, back_'a) | List.Nil => Result.fail .panic -/- [paper::sum]: forward function +/- [paper::sum]: Source: 'src/paper.rs', lines 57:0-57:32 -/ divergent def sum (l : List I32) : Result I32 := match l with | List.Cons x tl => do - let i ← sum tl - x + i + let i ← sum tl + x + i | List.Nil => Result.ret 0#i32 -/- [paper::test_nth]: forward function +/- [paper::test_nth]: Source: 'src/paper.rs', lines 68:0-68:17 -/ def test_nth : Result Unit := do - let l := List.Nil - let l0 := List.Cons 3#i32 l - let l1 := List.Cons 2#i32 l0 - let x ← list_nth_mut I32 (List.Cons 1#i32 l1) 2#u32 - let x0 ← x + 1#i32 - let l2 ← list_nth_mut_back I32 (List.Cons 1#i32 l1) 2#u32 x0 - let i ← sum l2 - if not (i = 7#i32) - then Result.fail .panic - else Result.ret () + let l := List.Nil + let l1 := List.Cons 3#i32 l + let l2 := List.Cons 2#i32 l1 + let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1#i32 l2) 2#u32 + let x1 ← x + 1#i32 + let l3 ← list_nth_mut_back x1 + let i ← sum l3 + if not (i = 7#i32) + then Result.fail .panic + else Result.ret () /- Unit test for [paper::test_nth] -/ #assert (test_nth == Result.ret ()) -/- [paper::call_choose]: forward function +/- [paper::call_choose]: Source: 'src/paper.rs', lines 76:0-76:44 -/ def call_choose (p : (U32 × U32)) : Result U32 := do - let (px, py) := p - let pz ← choose U32 true px py - let pz0 ← pz + 1#u32 - let (px0, _) ← choose_back U32 true px py pz0 - Result.ret px0 + let (px, py) := p + let (pz, choose_back) ← choose U32 true px py + let pz1 ← pz + 1#u32 + let (px1, _) ← choose_back pz1 + Result.ret px1 end paper diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index 37f0dffb..a485adbe 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -11,28 +11,29 @@ inductive List (T : Type) := | Cons : T → List T → List T | Nil : List T -/- [polonius_list::get_list_at_x]: forward function +/- [polonius_list::get_list_at_x]: Source: 'src/polonius_list.rs', lines 13:0-13:76 -/ -divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) := +divergent def get_list_at_x + (ls : List U32) (x : U32) : + Result ((List U32) × (List U32 → Result (List U32))) + := match ls with | List.Cons hd tl => if hd = x - then Result.ret (List.Cons hd tl) - else get_list_at_x tl x - | List.Nil => Result.ret List.Nil - -/- [polonius_list::get_list_at_x]: backward function 0 - Source: 'src/polonius_list.rs', lines 13:0-13:76 -/ -divergent def get_list_at_x_back - (ls : List U32) (x : U32) (ret : List U32) : Result (List U32) := - match ls with - | List.Cons hd tl => - if hd = x - then Result.ret ret + then + let back_'a := fun ret => Result.ret ret + Result.ret (List.Cons hd tl, back_'a) else do - let tl0 ← get_list_at_x_back tl x ret - Result.ret (List.Cons hd tl0) - | List.Nil => Result.ret ret + let (l, get_list_at_x_back) ← get_list_at_x tl x + let back_'a := + fun ret => + do + let tl1 ← get_list_at_x_back ret + Result.ret (List.Cons hd tl1) + Result.ret (l, back_'a) + | List.Nil => + let back_'a := fun ret => Result.ret ret + Result.ret (List.Nil, back_'a) end polonius_list diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 17118203..63d07d85 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -10,7 +10,7 @@ namespace traits structure BoolTrait (Self : Type) where get_bool : Self → Result Bool -/- [traits::{bool}::get_bool]: forward function +/- [traits::{bool}::get_bool]: Source: 'src/traits.rs', lines 12:4-12:30 -/ def Bool.get_bool (self : Bool) : Result Bool := Result.ret self @@ -21,27 +21,27 @@ def traits.BoolTraitBoolInst : BoolTrait Bool := { get_bool := Bool.get_bool } -/- [traits::BoolTrait::ret_true]: forward function +/- [traits::BoolTrait::ret_true]: Source: 'src/traits.rs', lines 6:4-6:30 -/ def BoolTrait.ret_true {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := Result.ret true -/- [traits::test_bool_trait_bool]: forward function +/- [traits::test_bool_trait_bool]: Source: 'src/traits.rs', lines 17:0-17:44 -/ def test_bool_trait_bool (x : Bool) : Result Bool := do - let b ← Bool.get_bool x - if b - then BoolTrait.ret_true traits.BoolTraitBoolInst x - else Result.ret false + let b ← Bool.get_bool x + if b + then BoolTrait.ret_true traits.BoolTraitBoolInst x + else Result.ret false -/- [traits::{core::option::Option<T>#1}::get_bool]: forward function +/- [traits::{core::option::Option<T>#1}::get_bool]: Source: 'src/traits.rs', lines 23:4-23:30 -/ def Option.get_bool (T : Type) (self : Option T) : Result Bool := match self with | none => Result.ret false - | some t => Result.ret true + | some _ => Result.ret true /- Trait implementation: [traits::{core::option::Option<T>#1}] Source: 'src/traits.rs', lines 22:0-22:31 -/ @@ -50,16 +50,16 @@ def traits.BoolTraitcoreoptionOptionTInst (T : Type) : BoolTrait (Option T) get_bool := Option.get_bool T } -/- [traits::test_bool_trait_option]: forward function +/- [traits::test_bool_trait_option]: Source: 'src/traits.rs', lines 31:0-31:54 -/ def test_bool_trait_option (T : Type) (x : Option T) : Result Bool := do - let b ← Option.get_bool T x - if b - then BoolTrait.ret_true (traits.BoolTraitcoreoptionOptionTInst T) x - else Result.ret false + let b ← Option.get_bool T x + if b + then BoolTrait.ret_true (traits.BoolTraitcoreoptionOptionTInst T) x + else Result.ret false -/- [traits::test_bool_trait]: forward function +/- [traits::test_bool_trait]: Source: 'src/traits.rs', lines 35:0-35:50 -/ def test_bool_trait (T : Type) (BoolTraitTInst : BoolTrait T) (x : T) : Result Bool := @@ -70,7 +70,7 @@ def test_bool_trait structure ToU64 (Self : Type) where to_u64 : Self → Result U64 -/- [traits::{u64#2}::to_u64]: forward function +/- [traits::{u64#2}::to_u64]: Source: 'src/traits.rs', lines 44:4-44:26 -/ def U64.to_u64 (self : U64) : Result U64 := Result.ret self @@ -81,15 +81,15 @@ def traits.ToU64U64Inst : ToU64 U64 := { to_u64 := U64.to_u64 } -/- [traits::{(A, A)#3}::to_u64]: forward function +/- [traits::{(A, A)#3}::to_u64]: Source: 'src/traits.rs', lines 50:4-50:26 -/ def Pair.to_u64 (A : Type) (ToU64AInst : ToU64 A) (self : (A × A)) : Result U64 := do - let (t, t0) := self - let i ← ToU64AInst.to_u64 t - let i0 ← ToU64AInst.to_u64 t0 - i + i0 + let (t, t1) := self + let i ← ToU64AInst.to_u64 t + let i1 ← ToU64AInst.to_u64 t1 + i + i1 /- Trait implementation: [traits::{(A, A)#3}] Source: 'src/traits.rs', lines 49:0-49:31 -/ @@ -98,18 +98,18 @@ def traits.ToU64TupleAAInst (A : Type) (ToU64AInst : ToU64 A) : ToU64 (A × A) to_u64 := Pair.to_u64 A ToU64AInst } -/- [traits::f]: forward function +/- [traits::f]: Source: 'src/traits.rs', lines 55:0-55:36 -/ def f (T : Type) (ToU64TInst : ToU64 T) (x : (T × T)) : Result U64 := Pair.to_u64 T ToU64TInst x -/- [traits::g]: forward function +/- [traits::g]: Source: 'src/traits.rs', lines 59:0-61:18 -/ def g (T : Type) (ToU64TupleTTInst : ToU64 (T × T)) (x : (T × T)) : Result U64 := ToU64TupleTTInst.to_u64 x -/- [traits::h0]: forward function +/- [traits::h0]: Source: 'src/traits.rs', lines 66:0-66:24 -/ def h0 (x : U64) : Result U64 := U64.to_u64 x @@ -119,7 +119,7 @@ def h0 (x : U64) : Result U64 := structure Wrapper (T : Type) where x : T -/- [traits::{traits::Wrapper<T>#4}::to_u64]: forward function +/- [traits::{traits::Wrapper<T>#4}::to_u64]: Source: 'src/traits.rs', lines 75:4-75:26 -/ def Wrapper.to_u64 (T : Type) (ToU64TInst : ToU64 T) (self : Wrapper T) : Result U64 := @@ -132,12 +132,12 @@ def traits.ToU64traitsWrapperTInst (T : Type) (ToU64TInst : ToU64 T) : ToU64 to_u64 := Wrapper.to_u64 T ToU64TInst } -/- [traits::h1]: forward function +/- [traits::h1]: Source: 'src/traits.rs', lines 80:0-80:33 -/ def h1 (x : Wrapper U64) : Result U64 := Wrapper.to_u64 U64 traits.ToU64U64Inst x -/- [traits::h2]: forward function +/- [traits::h2]: Source: 'src/traits.rs', lines 84:0-84:41 -/ def h2 (T : Type) (ToU64TInst : ToU64 T) (x : Wrapper T) : Result U64 := Wrapper.to_u64 T ToU64TInst x @@ -147,7 +147,7 @@ def h2 (T : Type) (ToU64TInst : ToU64 T) (x : Wrapper T) : Result U64 := structure ToType (Self T : Type) where to_type : Self → Result T -/- [traits::{u64#5}::to_type]: forward function +/- [traits::{u64#5}::to_type]: Source: 'src/traits.rs', lines 93:4-93:28 -/ def U64.to_type (self : U64) : Result Bool := Result.ret (self > 0#u64) @@ -164,7 +164,7 @@ structure OfType (Self : Type) where of_type : forall (T : Type) (ToTypeTSelfInst : ToType T Self), T → Result Self -/- [traits::h3]: forward function +/- [traits::h3]: Source: 'src/traits.rs', lines 104:0-104:50 -/ def h3 (T1 T2 : Type) (OfTypeT1Inst : OfType T1) (ToTypeT2T1Inst : ToType T2 T1) @@ -179,7 +179,7 @@ structure OfTypeBis (Self T : Type) where ToTypeTSelfInst : ToType T Self of_type : T → Result Self -/- [traits::h4]: forward function +/- [traits::h4]: Source: 'src/traits.rs', lines 118:0-118:57 -/ def h4 (T1 T2 : Type) (OfTypeBisT1T2Inst : OfTypeBis T1 T2) (ToTypeT2T1Inst : ToType @@ -201,7 +201,7 @@ def h4 structure TestType.test.TestTrait (Self : Type) where test : Self → Result Bool -/- [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]: forward function +/- [traits::{traits::TestType<T>#6}::test::{traits::{traits::TestType<T>#6}::test::TestType1}::test]: Source: 'src/traits.rs', lines 139:12-139:34 -/ def TestType.test.TestType1.test (self : TestType.test.TestType1) : Result Bool := @@ -214,23 +214,23 @@ def traits.TestType.test.TestTraittraitstraitsTestTypeTtestTestType1Inst : test := TestType.test.TestType1.test } -/- [traits::{traits::TestType<T>#6}::test]: forward function +/- [traits::{traits::TestType<T>#6}::test]: Source: 'src/traits.rs', lines 126:4-126:36 -/ def TestType.test (T : Type) (ToU64TInst : ToU64 T) (self : TestType T) (x : T) : Result Bool := do - let x0 ← ToU64TInst.to_u64 x - if x0 > 0#u64 - then TestType.test.TestType1.test 0#u64 - else Result.ret false + let x1 ← ToU64TInst.to_u64 x + if x1 > 0#u64 + then TestType.test.TestType1.test 0#u64 + else Result.ret false /- [traits::BoolWrapper] Source: 'src/traits.rs', lines 150:0-150:22 -/ @[reducible] def BoolWrapper := Bool -/- [traits::{traits::BoolWrapper#7}::to_type]: forward function +/- [traits::{traits::BoolWrapper#7}::to_type]: Source: 'src/traits.rs', lines 156:4-156:25 -/ def BoolWrapper.to_type (T : Type) (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) : @@ -266,8 +266,7 @@ structure WithConstTy (Self : Type) (LEN : Usize) where def bool_len1_body : Result Usize := Result.ret 12#usize def bool_len1_c : Usize := eval_global bool_len1_body (by simp) -/- [traits::{bool#8}::f]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) +/- [traits::{bool#8}::f]: Source: 'src/traits.rs', lines 180:4-180:39 -/ def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 := Result.ret i @@ -283,7 +282,7 @@ def traits.WithConstTyBool32Inst : WithConstTy Bool 32#usize := { f := Bool.f } -/- [traits::use_with_const_ty1]: forward function +/- [traits::use_with_const_ty1]: Source: 'src/traits.rs', lines 183:0-183:75 -/ def use_with_const_ty1 (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) : @@ -292,7 +291,7 @@ def use_with_const_ty1 let i := WithConstTyHLENInst.LEN1 Result.ret i -/- [traits::use_with_const_ty2]: forward function +/- [traits::use_with_const_ty2]: Source: 'src/traits.rs', lines 187:0-187:73 -/ def use_with_const_ty2 (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) @@ -301,7 +300,7 @@ def use_with_const_ty2 := Result.ret () -/- [traits::use_with_const_ty3]: forward function +/- [traits::use_with_const_ty3]: Source: 'src/traits.rs', lines 189:0-189:80 -/ def use_with_const_ty3 (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) @@ -310,12 +309,12 @@ def use_with_const_ty3 := WithConstTyHLENInst.W_clause_0.to_u64 x -/- [traits::test_where1]: forward function +/- [traits::test_where1]: Source: 'src/traits.rs', lines 193:0-193:40 -/ def test_where1 (T : Type) (_x : T) : Result Unit := Result.ret () -/- [traits::test_where2]: forward function +/- [traits::test_where2]: Source: 'src/traits.rs', lines 194:0-194:57 -/ def test_where2 (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) : @@ -340,22 +339,30 @@ structure ChildTrait (Self : Type) where ParentTrait0SelfInst : ParentTrait0 Self ParentTrait1SelfInst : ParentTrait1 Self -/- [traits::test_child_trait1]: forward function - Source: 'src/traits.rs', lines 209:0-209:56 -/ +/- [traits::test_parent_trait0]: + Source: 'src/traits.rs', lines 208:0-208:57 -/ +def test_parent_trait0 + (T : Type) (ParentTrait0TInst : ParentTrait0 T) (x : T) : + Result ParentTrait0TInst.W + := + ParentTrait0TInst.get_w x + +/- [traits::test_child_trait1]: + Source: 'src/traits.rs', lines 213:0-213:56 -/ def test_child_trait1 (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : Result String := ChildTraitTInst.ParentTrait0SelfInst.get_name x -/- [traits::test_child_trait2]: forward function - Source: 'src/traits.rs', lines 213:0-213:54 -/ +/- [traits::test_child_trait2]: + Source: 'src/traits.rs', lines 217:0-217:54 -/ def test_child_trait2 (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : Result ChildTraitTInst.ParentTrait0SelfInst.W := ChildTraitTInst.ParentTrait0SelfInst.get_w x -/- [traits::order1]: forward function - Source: 'src/traits.rs', lines 219:0-219:59 -/ +/- [traits::order1]: + Source: 'src/traits.rs', lines 223:0-223:59 -/ def order1 (T U : Type) (ParentTrait0TInst : ParentTrait0 T) (ParentTrait0UInst : ParentTrait0 U) : @@ -364,28 +371,28 @@ def order1 Result.ret () /- Trait declaration: [traits::ChildTrait1] - Source: 'src/traits.rs', lines 222:0-222:35 -/ + Source: 'src/traits.rs', lines 226:0-226:35 -/ structure ChildTrait1 (Self : Type) where ParentTrait1SelfInst : ParentTrait1 Self /- Trait implementation: [traits::{usize#9}] - Source: 'src/traits.rs', lines 224:0-224:27 -/ + Source: 'src/traits.rs', lines 228:0-228:27 -/ def traits.ParentTrait1UsizeInst : ParentTrait1 Usize := { } /- Trait implementation: [traits::{usize#10}] - Source: 'src/traits.rs', lines 225:0-225:26 -/ + Source: 'src/traits.rs', lines 229:0-229:26 -/ def traits.ChildTrait1UsizeInst : ChildTrait1 Usize := { ParentTrait1SelfInst := traits.ParentTrait1UsizeInst } /- Trait declaration: [traits::Iterator] - Source: 'src/traits.rs', lines 229:0-229:18 -/ + Source: 'src/traits.rs', lines 233:0-233:18 -/ structure Iterator (Self : Type) where Item : Type /- Trait declaration: [traits::IntoIterator] - Source: 'src/traits.rs', lines 233:0-233:22 -/ + Source: 'src/traits.rs', lines 237:0-237:22 -/ structure IntoIterator (Self : Type) where Item : Type IntoIter : Type @@ -393,76 +400,86 @@ structure IntoIterator (Self : Type) where into_iter : Self → Result IntoIter /- Trait declaration: [traits::FromResidual] - Source: 'src/traits.rs', lines 250:0-250:21 -/ + Source: 'src/traits.rs', lines 254:0-254:21 -/ structure FromResidual (Self T : Type) where /- Trait declaration: [traits::Try] - Source: 'src/traits.rs', lines 246:0-246:48 -/ + Source: 'src/traits.rs', lines 250:0-250:48 -/ structure Try (Self : Type) where Residual : Type FromResidualSelftraitsTrySelfResidualInst : FromResidual Self Residual /- Trait declaration: [traits::WithTarget] - Source: 'src/traits.rs', lines 252:0-252:20 -/ + Source: 'src/traits.rs', lines 256:0-256:20 -/ structure WithTarget (Self : Type) where Target : Type /- Trait declaration: [traits::ParentTrait2] - Source: 'src/traits.rs', lines 256:0-256:22 -/ + Source: 'src/traits.rs', lines 260:0-260:22 -/ structure ParentTrait2 (Self : Type) where U : Type U_clause_0 : WithTarget U /- Trait declaration: [traits::ChildTrait2] - Source: 'src/traits.rs', lines 260:0-260:35 -/ + Source: 'src/traits.rs', lines 264:0-264:35 -/ structure ChildTrait2 (Self : Type) where ParentTrait2SelfInst : ParentTrait2 Self convert : ParentTrait2SelfInst.U → Result ParentTrait2SelfInst.U_clause_0.Target /- Trait implementation: [traits::{u32#11}] - Source: 'src/traits.rs', lines 264:0-264:23 -/ + Source: 'src/traits.rs', lines 268:0-268:23 -/ def traits.WithTargetU32Inst : WithTarget U32 := { Target := U32 } /- Trait implementation: [traits::{u32#12}] - Source: 'src/traits.rs', lines 268:0-268:25 -/ + Source: 'src/traits.rs', lines 272:0-272:25 -/ def traits.ParentTrait2U32Inst : ParentTrait2 U32 := { U := U32 U_clause_0 := traits.WithTargetU32Inst } -/- [traits::{u32#13}::convert]: forward function - Source: 'src/traits.rs', lines 273:4-273:29 -/ +/- [traits::{u32#13}::convert]: + Source: 'src/traits.rs', lines 277:4-277:29 -/ def U32.convert (x : U32) : Result U32 := Result.ret x /- Trait implementation: [traits::{u32#13}] - Source: 'src/traits.rs', lines 272:0-272:24 -/ + Source: 'src/traits.rs', lines 276:0-276:24 -/ def traits.ChildTrait2U32Inst : ChildTrait2 U32 := { ParentTrait2SelfInst := traits.ParentTrait2U32Inst convert := U32.convert } /- Trait declaration: [traits::CFnOnce] - Source: 'src/traits.rs', lines 286:0-286:23 -/ + Source: 'src/traits.rs', lines 290:0-290:23 -/ structure CFnOnce (Self Args : Type) where Output : Type call_once : Self → Args → Result Output /- Trait declaration: [traits::CFnMut] - Source: 'src/traits.rs', lines 292:0-292:37 -/ + Source: 'src/traits.rs', lines 296:0-296:37 -/ structure CFnMut (Self Args : Type) where CFnOnceSelfArgsInst : CFnOnce Self Args - call_mut : Self → Args → Result CFnOnceSelfArgsInst.Output - call_mut_back : Self → Args → CFnOnceSelfArgsInst.Output → Result Self + call_mut : Self → Args → Result (CFnOnceSelfArgsInst.Output × Self) /- Trait declaration: [traits::CFn] - Source: 'src/traits.rs', lines 296:0-296:33 -/ + Source: 'src/traits.rs', lines 300:0-300:33 -/ structure CFn (Self Args : Type) where CFnMutSelfArgsInst : CFnMut Self Args - call_mut : Self → Args → Result - CFnMutSelfArgsInst.CFnOnceSelfArgsInst.Output + call : Self → Args → Result CFnMutSelfArgsInst.CFnOnceSelfArgsInst.Output + +/- Trait declaration: [traits::GetTrait] + Source: 'src/traits.rs', lines 304:0-304:18 -/ +structure GetTrait (Self : Type) where + W : Type + get_w : Self → Result W + +/- [traits::test_get_trait]: + Source: 'src/traits.rs', lines 309:0-309:49 -/ +def test_get_trait + (T : Type) (GetTraitTInst : GetTrait T) (x : T) : Result GetTraitTInst.W := + GetTraitTInst.get_w x end traits |