From 2b40c5c3de1ee2caca2c0072f812fea04b5a0238 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 14:59:10 +0200 Subject: tests: Merge the hashmap test files --- tests/lean/Hashmap/Funs.lean | 70 ++-- tests/lean/Hashmap/FunsExternal.lean | 19 + tests/lean/Hashmap/FunsExternal_Template.lean | 17 + tests/lean/Hashmap/Types.lean | 5 +- tests/lean/Hashmap/TypesExternal.lean | 7 + tests/lean/Hashmap/TypesExternal_Template.lean | 9 + tests/lean/HashmapMain.lean | 1 - tests/lean/HashmapMain/Funs.lean | 463 --------------------- tests/lean/HashmapMain/FunsExternal.lean | 17 - tests/lean/HashmapMain/FunsExternal_Template.lean | 18 - tests/lean/HashmapMain/Opaque.lean | 18 - tests/lean/HashmapMain/Types.lean | 23 - tests/lean/HashmapMain/TypesExternal.lean | 7 - tests/lean/HashmapMain/TypesExternal_Template.lean | 9 - tests/lean/lakefile.lean | 1 - 15 files changed, 95 insertions(+), 589 deletions(-) create mode 100644 tests/lean/Hashmap/FunsExternal.lean create mode 100644 tests/lean/Hashmap/FunsExternal_Template.lean create mode 100644 tests/lean/Hashmap/TypesExternal.lean create mode 100644 tests/lean/Hashmap/TypesExternal_Template.lean delete mode 100644 tests/lean/HashmapMain.lean delete mode 100644 tests/lean/HashmapMain/Funs.lean delete mode 100644 tests/lean/HashmapMain/FunsExternal.lean delete mode 100644 tests/lean/HashmapMain/FunsExternal_Template.lean delete mode 100644 tests/lean/HashmapMain/Opaque.lean delete mode 100644 tests/lean/HashmapMain/Types.lean delete mode 100644 tests/lean/HashmapMain/TypesExternal.lean delete mode 100644 tests/lean/HashmapMain/TypesExternal_Template.lean (limited to 'tests/lean') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 4f05fbc8..e76912cc 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -2,17 +2,18 @@ -- [hashmap]: function definitions import Base import Hashmap.Types +import Hashmap.FunsExternal open Primitives namespace hashmap /- [hashmap::hash_key]: - Source: 'tests/src/hashmap.rs', lines 35:0-35:32 -/ + Source: 'tests/src/hashmap.rs', lines 37:0-37:32 -/ def hash_key (k : Usize) : Result Usize := Result.ok k /- [hashmap::{hashmap::HashMap}::allocate_slots]: loop 0: - Source: 'tests/src/hashmap.rs', lines 58:4-64:5 -/ + Source: 'tests/src/hashmap.rs', lines 60:4-66:5 -/ divergent def HashMap.allocate_slots_loop (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) : Result (alloc.vec.Vec (List T)) @@ -26,7 +27,7 @@ divergent def HashMap.allocate_slots_loop else Result.ok slots /- [hashmap::{hashmap::HashMap}::allocate_slots]: - Source: 'tests/src/hashmap.rs', lines 58:4-58:76 -/ + Source: 'tests/src/hashmap.rs', lines 60:4-60:76 -/ def HashMap.allocate_slots (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) : Result (alloc.vec.Vec (List T)) @@ -34,7 +35,7 @@ def HashMap.allocate_slots HashMap.allocate_slots_loop T slots n /- [hashmap::{hashmap::HashMap}::new_with_capacity]: - Source: 'tests/src/hashmap.rs', lines 67:4-71:13 -/ + Source: 'tests/src/hashmap.rs', lines 69:4-73:13 -/ def HashMap.new_with_capacity (T : Type) (capacity : Usize) (max_load_dividend : Usize) (max_load_divisor : Usize) : @@ -53,12 +54,12 @@ def HashMap.new_with_capacity } /- [hashmap::{hashmap::HashMap}::new]: - Source: 'tests/src/hashmap.rs', lines 83:4-83:24 -/ + Source: 'tests/src/hashmap.rs', lines 85:4-85:24 -/ def HashMap.new (T : Type) : Result (HashMap T) := HashMap.new_with_capacity T 32#usize 4#usize 5#usize /- [hashmap::{hashmap::HashMap}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 88:4-96:5 -/ + Source: 'tests/src/hashmap.rs', lines 90:4-98:5 -/ divergent def HashMap.clear_loop (T : Type) (slots : alloc.vec.Vec (List T)) (i : Usize) : Result (alloc.vec.Vec (List T)) @@ -76,19 +77,19 @@ divergent def HashMap.clear_loop else Result.ok slots /- [hashmap::{hashmap::HashMap}::clear]: - Source: 'tests/src/hashmap.rs', lines 88:4-88:27 -/ + Source: 'tests/src/hashmap.rs', lines 90:4-90:27 -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do let hm ← HashMap.clear_loop T self.slots 0#usize Result.ok { self with num_entries := 0#usize, slots := hm } /- [hashmap::{hashmap::HashMap}::len]: - Source: 'tests/src/hashmap.rs', lines 98:4-98:30 -/ + Source: 'tests/src/hashmap.rs', lines 100:4-100:30 -/ def HashMap.len (T : Type) (self : HashMap T) : Result Usize := Result.ok self.num_entries /- [hashmap::{hashmap::HashMap}::insert_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 105:4-122:5 -/ + Source: 'tests/src/hashmap.rs', lines 107:4-124:5 -/ divergent def HashMap.insert_in_list_loop (T : Type) (key : Usize) (value : T) (ls : List T) : Result (Bool × (List T)) @@ -104,7 +105,7 @@ divergent def HashMap.insert_in_list_loop | List.Nil => Result.ok (true, List.Cons key value List.Nil) /- [hashmap::{hashmap::HashMap}::insert_in_list]: - Source: 'tests/src/hashmap.rs', lines 105:4-105:71 -/ + Source: 'tests/src/hashmap.rs', lines 107:4-107:71 -/ def HashMap.insert_in_list (T : Type) (key : Usize) (value : T) (ls : List T) : Result (Bool × (List T)) @@ -112,7 +113,7 @@ def HashMap.insert_in_list HashMap.insert_in_list_loop T key value ls /- [hashmap::{hashmap::HashMap}::insert_no_resize]: - Source: 'tests/src/hashmap.rs', lines 125:4-125:54 -/ + Source: 'tests/src/hashmap.rs', lines 127:4-127:54 -/ def HashMap.insert_no_resize (T : Type) (self : HashMap T) (key : Usize) (value : T) : Result (HashMap T) @@ -136,7 +137,7 @@ def HashMap.insert_no_resize Result.ok { self with slots := v } /- [hashmap::{hashmap::HashMap}::move_elements_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 191:4-204:5 -/ + Source: 'tests/src/hashmap.rs', lines 193:4-206:5 -/ divergent def HashMap.move_elements_from_list_loop (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) := match ls with @@ -147,13 +148,13 @@ divergent def HashMap.move_elements_from_list_loop | List.Nil => Result.ok ntable /- [hashmap::{hashmap::HashMap}::move_elements_from_list]: - Source: 'tests/src/hashmap.rs', lines 191:4-191:72 -/ + Source: 'tests/src/hashmap.rs', lines 193:4-193: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}::move_elements]: loop 0: - Source: 'tests/src/hashmap.rs', lines 179:4-188:5 -/ + Source: 'tests/src/hashmap.rs', lines 181:4-190:5 -/ divergent def HashMap.move_elements_loop (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize) : @@ -174,7 +175,7 @@ divergent def HashMap.move_elements_loop else Result.ok (ntable, slots) /- [hashmap::{hashmap::HashMap}::move_elements]: - Source: 'tests/src/hashmap.rs', lines 179:4-179:95 -/ + Source: 'tests/src/hashmap.rs', lines 181:4-181:95 -/ def HashMap.move_elements (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize) : @@ -183,7 +184,7 @@ def HashMap.move_elements HashMap.move_elements_loop T ntable slots i /- [hashmap::{hashmap::HashMap}::try_resize]: - Source: 'tests/src/hashmap.rs', lines 148:4-148:28 -/ + Source: 'tests/src/hashmap.rs', lines 150:4-150:28 -/ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_u32_max @@ -207,7 +208,7 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := else Result.ok { self with max_load_factor := (i, i1) } /- [hashmap::{hashmap::HashMap}::insert]: - Source: 'tests/src/hashmap.rs', lines 137:4-137:48 -/ + Source: 'tests/src/hashmap.rs', lines 139:4-139:48 -/ def HashMap.insert (T : Type) (self : HashMap T) (key : Usize) (value : T) : Result (HashMap T) @@ -220,7 +221,7 @@ def HashMap.insert else Result.ok self1 /- [hashmap::{hashmap::HashMap}::contains_key_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 214:4-227:5 -/ + Source: 'tests/src/hashmap.rs', lines 216:4-229:5 -/ divergent def HashMap.contains_key_in_list_loop (T : Type) (key : Usize) (ls : List T) : Result Bool := match ls with @@ -231,13 +232,13 @@ divergent def HashMap.contains_key_in_list_loop | List.Nil => Result.ok false /- [hashmap::{hashmap::HashMap}::contains_key_in_list]: - Source: 'tests/src/hashmap.rs', lines 214:4-214:68 -/ + Source: 'tests/src/hashmap.rs', lines 216:4-216: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}::contains_key]: - Source: 'tests/src/hashmap.rs', lines 207:4-207:49 -/ + Source: 'tests/src/hashmap.rs', lines 209:4-209:49 -/ def HashMap.contains_key (T : Type) (self : HashMap T) (key : Usize) : Result Bool := do @@ -250,7 +251,7 @@ def HashMap.contains_key HashMap.contains_key_in_list T key l /- [hashmap::{hashmap::HashMap}::get_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 232:4-245:5 -/ + Source: 'tests/src/hashmap.rs', lines 234:4-247:5 -/ divergent def HashMap.get_in_list_loop (T : Type) (key : Usize) (ls : List T) : Result T := match ls with @@ -261,12 +262,12 @@ divergent def HashMap.get_in_list_loop | List.Nil => Result.fail .panic /- [hashmap::{hashmap::HashMap}::get_in_list]: - Source: 'tests/src/hashmap.rs', lines 232:4-232:70 -/ + Source: 'tests/src/hashmap.rs', lines 234:4-234: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}::get]: - Source: 'tests/src/hashmap.rs', lines 247:4-247:55 -/ + Source: 'tests/src/hashmap.rs', lines 249:4-249:55 -/ def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T := do let hash ← hash_key key @@ -278,7 +279,7 @@ def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T := HashMap.get_in_list T key l /- [hashmap::{hashmap::HashMap}::get_mut_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 253:4-262:5 -/ + Source: 'tests/src/hashmap.rs', lines 255:4-264:5 -/ divergent def HashMap.get_mut_in_list_loop (T : Type) (ls : List T) (key : Usize) : Result (T × (T → Result (List T))) @@ -301,7 +302,7 @@ divergent def HashMap.get_mut_in_list_loop | List.Nil => Result.fail .panic /- [hashmap::{hashmap::HashMap}::get_mut_in_list]: - Source: 'tests/src/hashmap.rs', lines 253:4-253:86 -/ + Source: 'tests/src/hashmap.rs', lines 255:4-255:86 -/ def HashMap.get_mut_in_list (T : Type) (ls : List T) (key : Usize) : Result (T × (T → Result (List T))) @@ -309,7 +310,7 @@ def HashMap.get_mut_in_list HashMap.get_mut_in_list_loop T ls key /- [hashmap::{hashmap::HashMap}::get_mut]: - Source: 'tests/src/hashmap.rs', lines 265:4-265:67 -/ + Source: 'tests/src/hashmap.rs', lines 267:4-267:67 -/ def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result (T × (T → Result (HashMap T))) @@ -331,7 +332,7 @@ def HashMap.get_mut Result.ok (t, back) /- [hashmap::{hashmap::HashMap}::remove_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 273:4-299:5 -/ + Source: 'tests/src/hashmap.rs', lines 275:4-301:5 -/ divergent def HashMap.remove_from_list_loop (T : Type) (key : Usize) (ls : List T) : Result ((Option T) × (List T)) := match ls with @@ -350,13 +351,13 @@ divergent def HashMap.remove_from_list_loop | List.Nil => Result.ok (none, List.Nil) /- [hashmap::{hashmap::HashMap}::remove_from_list]: - Source: 'tests/src/hashmap.rs', lines 273:4-273:69 -/ + Source: 'tests/src/hashmap.rs', lines 275:4-275:69 -/ 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}::remove]: - Source: 'tests/src/hashmap.rs', lines 302:4-302:52 -/ + Source: 'tests/src/hashmap.rs', lines 304:4-304:52 -/ def HashMap.remove (T : Type) (self : HashMap T) (key : Usize) : Result ((Option T) × (HashMap T)) @@ -380,8 +381,17 @@ def HashMap.remove let v ← index_mut_back l1 Result.ok (some x1, { self with num_entries := i1, slots := v }) +/- [hashmap::insert_on_disk]: + Source: 'tests/src/hashmap.rs', lines 335:0-335:43 -/ +def insert_on_disk + (key : Usize) (value : U64) (st : State) : Result (State × Unit) := + do + let (st1, hm) ← hashmap_utils.deserialize st + let hm1 ← HashMap.insert U64 hm key value + hashmap_utils.serialize hm1 st1 + /- [hashmap::test1]: - Source: 'tests/src/hashmap.rs', lines 323:0-323:10 -/ + Source: 'tests/src/hashmap.rs', lines 350:0-350:10 -/ def test1 : Result Unit := do let hm ← HashMap.new U64 diff --git a/tests/lean/Hashmap/FunsExternal.lean b/tests/lean/Hashmap/FunsExternal.lean new file mode 100644 index 00000000..7454696b --- /dev/null +++ b/tests/lean/Hashmap/FunsExternal.lean @@ -0,0 +1,19 @@ +-- [hashmap]: external functions. +import Base +import Hashmap.Types +open Primitives +open hashmap + +-- TODO: fill those bodies + +/- [hashmap::hashmap_utils::deserialize]: + Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/ +def hashmap_utils.deserialize + : State → Result (State × (HashMap U64)) := + fun _ => .fail .panic + +/- [hashmap::hashmap_utils::serialize]: + Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/ +def hashmap_utils.serialize + : HashMap U64 → State → Result (State × Unit) := + fun _ _ => .fail .panic diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean new file mode 100644 index 00000000..16b4b6af --- /dev/null +++ b/tests/lean/Hashmap/FunsExternal_Template.lean @@ -0,0 +1,17 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. +import Base +import Hashmap.Types +open Primitives +open hashmap + +/- [hashmap::hashmap_utils::deserialize]: + Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/ +axiom hashmap_utils.deserialize : State → Result (State × (HashMap U64)) + +/- [hashmap::hashmap_utils::serialize]: + Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/ +axiom hashmap_utils.serialize + : HashMap U64 → State → Result (State × Unit) + diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index a98b972f..b4301106 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -1,18 +1,19 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [hashmap]: type definitions import Base +import Hashmap.TypesExternal open Primitives namespace hashmap /- [hashmap::List] - Source: 'tests/src/hashmap.rs', lines 27:0-27:16 -/ + Source: 'tests/src/hashmap.rs', lines 29:0-29:16 -/ inductive List (T : Type) := | Cons : Usize → T → List T → List T | Nil : List T /- [hashmap::HashMap] - Source: 'tests/src/hashmap.rs', lines 43:0-43:21 -/ + Source: 'tests/src/hashmap.rs', lines 45:0-45:21 -/ structure HashMap (T : Type) where num_entries : Usize max_load_factor : (Usize × Usize) diff --git a/tests/lean/Hashmap/TypesExternal.lean b/tests/lean/Hashmap/TypesExternal.lean new file mode 100644 index 00000000..b32c4c42 --- /dev/null +++ b/tests/lean/Hashmap/TypesExternal.lean @@ -0,0 +1,7 @@ +-- [hashmap]: external types. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/Hashmap/TypesExternal_Template.lean b/tests/lean/Hashmap/TypesExternal_Template.lean new file mode 100644 index 00000000..03c3d157 --- /dev/null +++ b/tests/lean/Hashmap/TypesExternal_Template.lean @@ -0,0 +1,9 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/HashmapMain.lean b/tests/lean/HashmapMain.lean deleted file mode 100644 index 1a4e7f82..00000000 --- a/tests/lean/HashmapMain.lean +++ /dev/null @@ -1 +0,0 @@ -import HashmapMain.Funs diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean deleted file mode 100644 index 45d6b058..00000000 --- a/tests/lean/HashmapMain/Funs.lean +++ /dev/null @@ -1,463 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: function definitions -import Base -import HashmapMain.Types -import HashmapMain.FunsExternal -open Primitives - -namespace hashmap_main - -/- [hashmap_main::hashmap::hash_key]: - Source: 'tests/src/hashmap.rs', lines 35:0-35:32 -/ -def hashmap.hash_key (k : Usize) : Result Usize := - Result.ok k - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: loop 0: - Source: 'tests/src/hashmap.rs', lines 58:4-64:5 -/ -divergent def hashmap.HashMap.allocate_slots_loop - (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) : - Result (alloc.vec.Vec (hashmap.List T)) - := - if n > 0#usize - then - do - let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil - let n1 ← n - 1#usize - hashmap.HashMap.allocate_slots_loop T slots1 n1 - else Result.ok slots - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: - Source: 'tests/src/hashmap.rs', lines 58:4-58:76 -/ -def hashmap.HashMap.allocate_slots - (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) : - Result (alloc.vec.Vec (hashmap.List T)) - := - hashmap.HashMap.allocate_slots_loop T slots n - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new_with_capacity]: - Source: 'tests/src/hashmap.rs', lines 67:4-71:13 -/ -def hashmap.HashMap.new_with_capacity - (T : Type) (capacity : Usize) (max_load_dividend : Usize) - (max_load_divisor : Usize) : - Result (hashmap.HashMap T) - := - do - let slots ← - hashmap.HashMap.allocate_slots T (alloc.vec.Vec.new (hashmap.List T)) - capacity - let i ← capacity * max_load_dividend - let i1 ← i / max_load_divisor - Result.ok - { - 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}::new]: - Source: 'tests/src/hashmap.rs', lines 83:4-83: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}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 88:4-96: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 i1 := alloc.vec.Vec.len (hashmap.List T) slots - if i < i1 - then - do - 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.ok slots - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: - Source: 'tests/src/hashmap.rs', lines 88:4-88:27 -/ -def hashmap.HashMap.clear - (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) := - do - let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize - Result.ok { self with num_entries := 0#usize, slots := hm } - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: - Source: 'tests/src/hashmap.rs', lines 98:4-98:30 -/ -def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize := - Result.ok self.num_entries - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 105:4-122:5 -/ -divergent def hashmap.HashMap.insert_in_list_loop - (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : - Result (Bool × (hashmap.List T)) - := - match ls with - | hashmap.List.Cons ckey cvalue tl => - if ckey = key - then Result.ok (false, hashmap.List.Cons ckey value tl) - else - do - let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl - Result.ok (b, hashmap.List.Cons ckey cvalue tl1) - | hashmap.List.Nil => - Result.ok (true, hashmap.List.Cons key value hashmap.List.Nil) - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: - Source: 'tests/src/hashmap.rs', lines 105:4-105:71 -/ -def hashmap.HashMap.insert_in_list - (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) : - Result (Bool × (hashmap.List T)) - := - hashmap.HashMap.insert_in_list_loop T key value ls - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_no_resize]: - Source: 'tests/src/hashmap.rs', lines 125:4-125: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, 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.ok { self with num_entries := i1, slots := v } - else do - let v ← index_mut_back l1 - Result.ok { self with slots := v } - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 191:4-204:5 -/ -divergent def hashmap.HashMap.move_elements_from_list_loop - (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : - Result (hashmap.HashMap T) - := - match ls with - | hashmap.List.Cons k v tl => - do - let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v - hashmap.HashMap.move_elements_from_list_loop T ntable1 tl - | hashmap.List.Nil => Result.ok ntable - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: - Source: 'tests/src/hashmap.rs', lines 191:4-191:72 -/ -def hashmap.HashMap.move_elements_from_list - (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) : - Result (hashmap.HashMap T) - := - hashmap.HashMap.move_elements_from_list_loop T ntable ls - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: loop 0: - Source: 'tests/src/hashmap.rs', lines 179:4-188: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 i1 := alloc.vec.Vec.len (hashmap.List T) slots - if i < i1 - then - do - 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 ntable1 ← hashmap.HashMap.move_elements_from_list T ntable ls - let i2 ← i + 1#usize - let slots1 ← index_mut_back l1 - hashmap.HashMap.move_elements_loop T ntable1 slots1 i2 - else Result.ok (ntable, slots) - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: - Source: 'tests/src/hashmap.rs', lines 179:4-179: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 - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::try_resize]: - Source: 'tests/src/hashmap.rs', lines 148:4-148: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, 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.ok - { - ntable1 - with - num_entries := self.num_entries, max_load_factor := (i, i1) - } - else Result.ok { self with max_load_factor := (i, i1) } - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert]: - Source: 'tests/src/hashmap.rs', lines 137:4-137:48 -/ -def hashmap.HashMap.insert - (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) : - Result (hashmap.HashMap T) - := - do - let self1 ← hashmap.HashMap.insert_no_resize T self key value - let i ← hashmap.HashMap.len T self1 - if i > self1.max_load - then hashmap.HashMap.try_resize T self1 - else Result.ok self1 - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 214:4-227: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 _ tl => - if ckey = key - then Result.ok true - else hashmap.HashMap.contains_key_in_list_loop T key tl - | hashmap.List.Nil => Result.ok false - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: - Source: 'tests/src/hashmap.rs', lines 214:4-214: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}::contains_key]: - Source: 'tests/src/hashmap.rs', lines 207:4-207: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}::get_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 232:4-245:5 -/ -divergent def hashmap.HashMap.get_in_list_loop - (T : Type) (key : Usize) (ls : hashmap.List T) : Result T := - match ls with - | hashmap.List.Cons ckey cvalue tl => - if ckey = key - then Result.ok cvalue - else hashmap.HashMap.get_in_list_loop T key tl - | hashmap.List.Nil => Result.fail .panic - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: - Source: 'tests/src/hashmap.rs', lines 232:4-232: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}::get]: - Source: 'tests/src/hashmap.rs', lines 247:4-247: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}::get_mut_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 253:4-262:5 -/ -divergent def hashmap.HashMap.get_mut_in_list_loop - (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 - let back := fun ret => Result.ok (hashmap.List.Cons ckey ret tl) - Result.ok (cvalue, back) - else - do - let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key - let back1 := - fun ret => - do - let tl1 ← back ret - Result.ok (hashmap.List.Cons ckey cvalue tl1) - Result.ok (t, back1) - | hashmap.List.Nil => Result.fail .panic - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: - Source: 'tests/src/hashmap.rs', lines 253:4-253:86 -/ -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 T ls key - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: - Source: 'tests/src/hashmap.rs', lines 265:4-265:67 -/ -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, 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 := - fun ret => - do - let l1 ← get_mut_in_list_back ret - let v ← index_mut_back l1 - Result.ok { self with slots := v } - Result.ok (t, back) - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 273:4-299:5 -/ -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, _) := - core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl) - hashmap.List.Nil - match mv_ls with - | hashmap.List.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1) - | hashmap.List.Nil => Result.fail .panic - else - do - let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl - Result.ok (o, hashmap.List.Cons ckey t tl1) - | hashmap.List.Nil => Result.ok (none, hashmap.List.Nil) - -/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: - Source: 'tests/src/hashmap.rs', lines 273:4-273:69 -/ -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}::remove]: - Source: 'tests/src/hashmap.rs', lines 302:4-302:52 -/ -def hashmap.HashMap.remove - (T : Type) (self : hashmap.HashMap T) (key : Usize) : - 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, 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.ok (none, { self with slots := v }) - | some x1 => - do - let i1 ← self.num_entries - 1#usize - let v ← index_mut_back l1 - Result.ok (some x1, { self with num_entries := i1, slots := v }) - -/- [hashmap_main::hashmap::test1]: - Source: 'tests/src/hashmap.rs', lines 323:0-323:10 -/ -def hashmap.test1 : Result Unit := - do - 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 ¬ (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 ¬ (i1 = 56#u64) - then Result.fail .panic - else - do - let (x, hm6) ← hashmap.HashMap.remove U64 hm5 1024#usize - match x with - | none => Result.fail .panic - | some x1 => - if ¬ (x1 = 56#u64) - then Result.fail .panic - else - do - let i2 ← hashmap.HashMap.get U64 hm6 0#usize - if ¬ (i2 = 42#u64) - then Result.fail .panic - else - do - let i3 ← hashmap.HashMap.get U64 hm6 128#usize - if ¬ (i3 = 18#u64) - then Result.fail .panic - else - do - let i4 ← hashmap.HashMap.get U64 hm6 1056#usize - if ¬ (i4 = 256#u64) - then Result.fail .panic - else Result.ok () - -/- [hashmap_main::insert_on_disk]: - Source: 'tests/src/hashmap_main.rs', lines 13:0-13:43 -/ -def insert_on_disk - (key : Usize) (value : U64) (st : State) : Result (State × Unit) := - do - let (st1, hm) ← hashmap_utils.deserialize st - let hm1 ← hashmap.HashMap.insert U64 hm key value - hashmap_utils.serialize hm1 st1 - -/- [hashmap_main::main]: - Source: 'tests/src/hashmap_main.rs', lines 22:0-22:13 -/ -def main : Result Unit := - Result.ok () - -end hashmap_main diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean deleted file mode 100644 index b394b32b..00000000 --- a/tests/lean/HashmapMain/FunsExternal.lean +++ /dev/null @@ -1,17 +0,0 @@ --- [hashmap_main]: templates for the external functions. -import Base -import HashmapMain.Types -open Primitives -open hashmap_main - --- TODO: fill those bodies - -/- [hashmap_main::hashmap_utils::deserialize] -/ -def hashmap_utils.deserialize - : State → Result (State × (hashmap.HashMap U64)) := - fun _ => .fail .panic - -/- [hashmap_main::hashmap_utils::serialize] -/ -def hashmap_utils.serialize - : hashmap.HashMap U64 → State → Result (State × Unit) := - fun _ _ => .fail .panic diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean deleted file mode 100644 index 1a6c40d5..00000000 --- a/tests/lean/HashmapMain/FunsExternal_Template.lean +++ /dev/null @@ -1,18 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: external functions. --- This is a template file: rename it to "FunsExternal.lean" and fill the holes. -import Base -import HashmapMain.Types -open Primitives -open hashmap_main - -/- [hashmap_main::hashmap_utils::deserialize]: - Source: 'tests/src/hashmap_utils.rs', lines 11:0-11:43 -/ -axiom hashmap_utils.deserialize - : State → Result (State × (hashmap.HashMap U64)) - -/- [hashmap_main::hashmap_utils::serialize]: - Source: 'tests/src/hashmap_utils.rs', lines 6:0-6:42 -/ -axiom hashmap_utils.serialize - : hashmap.HashMap U64 → State → Result (State × Unit) - diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean deleted file mode 100644 index a410b253..00000000 --- a/tests/lean/HashmapMain/Opaque.lean +++ /dev/null @@ -1,18 +0,0 @@ --- [hashmap_main]: opaque function definitions -import Base -import HashmapMain.Types -open Primitives - -namespace hashmap_main - -structure OpaqueDefs where - - /- [hashmap_main::hashmap_utils::deserialize] -/ - hashmap_utils.deserialize_fwd - : State → Result (State × (hashmap_hash_map_t U64)) - - /- [hashmap_main::hashmap_utils::serialize] -/ - hashmap_utils.serialize_fwd - : hashmap_hash_map_t U64 → State → Result (State × Unit) - -end hashmap_main diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean deleted file mode 100644 index 54f11e1e..00000000 --- a/tests/lean/HashmapMain/Types.lean +++ /dev/null @@ -1,23 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: type definitions -import Base -import HashmapMain.TypesExternal -open Primitives - -namespace hashmap_main - -/- [hashmap_main::hashmap::List] - Source: 'tests/src/hashmap.rs', lines 27:0-27:16 -/ -inductive hashmap.List (T : Type) := -| Cons : Usize → T → hashmap.List T → hashmap.List T -| Nil : hashmap.List T - -/- [hashmap_main::hashmap::HashMap] - Source: 'tests/src/hashmap.rs', lines 43:0-43:21 -/ -structure hashmap.HashMap (T : Type) where - num_entries : Usize - max_load_factor : (Usize × Usize) - max_load : Usize - slots : alloc.vec.Vec (hashmap.List T) - -end hashmap_main diff --git a/tests/lean/HashmapMain/TypesExternal.lean b/tests/lean/HashmapMain/TypesExternal.lean deleted file mode 100644 index 4e1cdbe9..00000000 --- a/tests/lean/HashmapMain/TypesExternal.lean +++ /dev/null @@ -1,7 +0,0 @@ --- [hashmap_main]: external types. -import Base -open Primitives - -/- The state type used in the state-error monad -/ -axiom State : Type - diff --git a/tests/lean/HashmapMain/TypesExternal_Template.lean b/tests/lean/HashmapMain/TypesExternal_Template.lean deleted file mode 100644 index cfa8bbb1..00000000 --- a/tests/lean/HashmapMain/TypesExternal_Template.lean +++ /dev/null @@ -1,9 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: external types. --- This is a template file: rename it to "TypesExternal.lean" and fill the holes. -import Base -open Primitives - -/- The state type used in the state-error monad -/ -axiom State : Type - diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index 3a777824..bb13ddf2 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -13,7 +13,6 @@ package «tests» {} @[default_target] lean_lib Constants @[default_target] lean_lib External @[default_target] lean_lib Hashmap -@[default_target] lean_lib HashmapMain @[default_target] lean_lib Loops @[default_target] lean_lib NoNestedBorrows @[default_target] lean_lib Paper -- cgit v1.2.3 From f77e3f9cbe2ea7abeb4be815bdbf33d0c98076c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 13:28:28 +0200 Subject: tests: Rename betree_main -> betree --- tests/lean/Betree/Funs.lean | 699 ++++++++++++++++++++++ tests/lean/Betree/FunsExternal.lean | 30 + tests/lean/Betree/FunsExternal_Template.lean | 30 + tests/lean/Betree/Types.lean | 83 +++ tests/lean/Betree/TypesExternal.lean | 7 + tests/lean/Betree/TypesExternal_Template.lean | 9 + tests/lean/BetreeMain.lean | 1 - tests/lean/BetreeMain/Funs.lean | 699 ---------------------- tests/lean/BetreeMain/FunsExternal.lean | 30 - tests/lean/BetreeMain/FunsExternal_Template.lean | 30 - tests/lean/BetreeMain/Types.lean | 83 --- tests/lean/BetreeMain/TypesExternal.lean | 7 - tests/lean/BetreeMain/TypesExternal_Template.lean | 9 - tests/lean/lakefile.lean | 2 +- 14 files changed, 859 insertions(+), 860 deletions(-) create mode 100644 tests/lean/Betree/Funs.lean create mode 100644 tests/lean/Betree/FunsExternal.lean create mode 100644 tests/lean/Betree/FunsExternal_Template.lean create mode 100644 tests/lean/Betree/Types.lean create mode 100644 tests/lean/Betree/TypesExternal.lean create mode 100644 tests/lean/Betree/TypesExternal_Template.lean delete mode 100644 tests/lean/BetreeMain.lean delete mode 100644 tests/lean/BetreeMain/Funs.lean delete mode 100644 tests/lean/BetreeMain/FunsExternal.lean delete mode 100644 tests/lean/BetreeMain/FunsExternal_Template.lean delete mode 100644 tests/lean/BetreeMain/Types.lean delete mode 100644 tests/lean/BetreeMain/TypesExternal.lean delete mode 100644 tests/lean/BetreeMain/TypesExternal_Template.lean (limited to 'tests/lean') diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean new file mode 100644 index 00000000..8612ccbc --- /dev/null +++ b/tests/lean/Betree/Funs.lean @@ -0,0 +1,699 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree]: function definitions +import Base +import Betree.Types +import Betree.FunsExternal +open Primitives + +namespace betree + +/- [betree::betree::load_internal_node]: + Source: 'src/betree.rs', lines 36:0-36:52 -/ +def betree.load_internal_node + (id : U64) (st : State) : + Result (State × (betree.List (U64 × betree.Message))) + := + betree_utils.load_internal_node id st + +/- [betree::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) + := + betree_utils.store_internal_node id content st + +/- [betree::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::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) + := + betree_utils.store_leaf_node id content st + +/- [betree::betree::fresh_node_id]: + Source: 'src/betree.rs', lines 55:0-55:48 -/ +def betree.fresh_node_id (counter : U64) : Result (U64 × U64) := + do + let counter1 ← counter + 1#u64 + Result.ok (counter, counter1) + +/- [betree::betree::{betree::betree::NodeIdCounter}::new]: + Source: 'src/betree.rs', lines 206:4-206:20 -/ +def betree.NodeIdCounter.new : Result betree.NodeIdCounter := + Result.ok { next_node_id := 0#u64 } + +/- [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: + Source: 'src/betree.rs', lines 210:4-210:36 -/ +def betree.NodeIdCounter.fresh_id + (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) := + do + let i ← self.next_node_id + 1#u64 + Result.ok (self.next_node_id, { next_node_id := i }) + +/- [betree::betree::upsert_update]: + Source: 'src/betree.rs', lines 234:0-234:70 -/ +def betree.upsert_update + (prev : Option U64) (st : betree.UpsertFunState) : Result U64 := + match prev with + | none => + match st with + | betree.UpsertFunState.Add v => Result.ok v + | betree.UpsertFunState.Sub _ => Result.ok 0#u64 + | some prev1 => + match st with + | betree.UpsertFunState.Add v => + do + let margin ← core_u64_max - prev1 + if margin >= v + then prev1 + v + else Result.ok core_u64_max + | betree.UpsertFunState.Sub v => + if prev1 >= v + then prev1 - v + else Result.ok 0#u64 + +/- [betree::betree::{betree::betree::List#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 _ tl => do + let i ← betree.List.len T tl + 1#u64 + i + | betree.List.Nil => Result.ok 0#u64 + +/- [betree::betree::{betree::betree::List#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) : + Result ((betree.List T) × (betree.List T)) + := + if n = 0#u64 + then Result.ok (betree.List.Nil, self) + else + 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 + Result.ok (betree.List.Cons hd ls0, ls1) + | betree.List.Nil => Result.fail .panic + +/- [betree::betree::{betree::betree::List#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 + Result.ok (betree.List.Cons x tl) + +/- [betree::betree::{betree::betree::List#1}::pop_front]: + Source: 'src/betree.rs', lines 306:4-306:32 -/ +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.ok (x, tl) + | betree.List.Nil => Result.fail .panic + +/- [betree::betree::{betree::betree::List#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 _ => Result.ok hd + | betree.List.Nil => Result.fail .panic + +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: + Source: 'src/betree.rs', lines 327:4-327:44 -/ +def betree.ListPairU64T.head_has_key + (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := + match self with + | betree.List.Cons hd _ => let (i, _) := hd + Result.ok (i = key) + | betree.List.Nil => Result.ok false + +/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 339:4-339:73 -/ +divergent def betree.ListPairU64T.partition_at_pivot + (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : + Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) + := + match self with + | betree.List.Cons hd tl => + let (i, t) := hd + if i >= pivot + then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl) + else + do + let p ← betree.ListPairU64T.partition_at_pivot T tl pivot + let (ls0, ls1) := p + Result.ok (betree.List.Cons (i, t) ls0, ls1) + | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil) + +/- [betree::betree::{betree::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 × betree.NodeIdCounter)) + := + do + 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, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1 + 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.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) + +/- [betree::betree::{betree::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)) × (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.ok (betree.List.Cons (i, m) next_msgs, Result.ok) + else + do + let (l, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key next_msgs + let back := + fun ret => + do + let next_msgs1 ← lookup_first_message_for_key_back ret + Result.ok (betree.List.Cons (i, m) next_msgs1) + Result.ok (l, back) + | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) + +/- [betree::betree::{betree::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, i1) := hd + if i = key + then Result.ok (some i1) + else + if i > key + then Result.ok none + else betree.Node.lookup_in_bindings key tl + | betree.List.Nil => Result.ok none + +/- [betree::betree::{betree::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) + : + Result (U64 × (betree.List (U64 × betree.Message))) + := + do + let b ← betree.ListPairU64T.head_has_key betree.Message msgs key + if b + then + do + let (msg, msgs1) ← 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 ← betree.upsert_update prev s + betree.Node.apply_upserts msgs1 (some v) key + else + do + let v ← core.option.Option.unwrap U64 prev + let msgs1 ← + betree.List.push_front (U64 × betree.Message) msgs (key, + betree.Message.Insert v) + Result.ok (v, msgs1) + +/- [betree::betree::{betree::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) × betree.Internal)) + := + if key < self.pivot + then + do + let (st1, (o, n)) ← betree.Node.lookup self.left key st + Result.ok (st1, (o, betree.Internal.mk self.id self.pivot n self.right)) + else + do + let (st1, (o, n)) ← betree.Node.lookup self.right key st + Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n)) + +/- [betree::betree::{betree::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) × betree.Node)) + := + match self with + | betree.Node.Internal node => + do + let (st1, msgs) ← betree.load_internal_node node.id 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 (st2, (o, node1)) ← + betree.Internal.lookup_in_children node key st1 + let _ ← + lookup_first_message_for_key_back (betree.List.Cons (k, msg) l) + Result.ok (st2, (o, betree.Node.Internal node1)) + else + match msg with + | betree.Message.Insert v => + do + let _ ← + lookup_first_message_for_key_back (betree.List.Cons (k, + betree.Message.Insert v) l) + Result.ok (st1, (some v, betree.Node.Internal node)) + | betree.Message.Delete => + do + let _ ← + lookup_first_message_for_key_back (betree.List.Cons (k, + betree.Message.Delete) l) + Result.ok (st1, (none, betree.Node.Internal node)) + | betree.Message.Upsert ufs => + do + let (st2, (v, node1)) ← + betree.Internal.lookup_in_children node key st1 + let (v1, pending1) ← + betree.Node.apply_upserts (betree.List.Cons (k, + betree.Message.Upsert ufs) l) v key + let msgs1 ← lookup_first_message_for_key_back pending1 + let (st3, _) ← betree.store_internal_node node1.id msgs1 st2 + Result.ok (st3, (some v1, betree.Node.Internal node1)) + | betree.List.Nil => + do + let (st2, (o, node1)) ← betree.Internal.lookup_in_children node key st1 + let _ ← lookup_first_message_for_key_back betree.List.Nil + Result.ok (st2, (o, betree.Node.Internal node1)) + | betree.Node.Leaf node => + do + let (st1, bindings) ← betree.load_leaf_node node.id st + let o ← betree.Node.lookup_in_bindings key bindings + Result.ok (st1, (o, betree.Node.Leaf node)) + +end + +/- [betree::betree::{betree::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)) : + Result (betree.List (U64 × betree.Message)) + := + match msgs with + | betree.List.Cons p l => + let (k, m) := p + if k = key + then + do + let (_, msgs1) ← + betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) + l) + betree.Node.filter_messages_for_key key msgs1 + else Result.ok (betree.List.Cons (k, m) l) + | betree.List.Nil => Result.ok betree.List.Nil + +/- [betree::betree::{betree::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)) × (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 + do + let (l, lookup_first_message_after_key_back) ← + betree.Node.lookup_first_message_after_key key next_msgs + let back := + fun ret => + do + let next_msgs1 ← lookup_first_message_after_key_back ret + Result.ok (betree.List.Cons (k, m) next_msgs1) + Result.ok (l, back) + else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok) + | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) + +/- [betree::betree::{betree::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) + (new_msg : betree.Message) : + Result (betree.List (U64 × betree.Message)) + := + do + let (msgs1, lookup_first_message_for_key_back) ← + betree.Node.lookup_first_message_for_key key msgs + let b ← betree.ListPairU64T.head_has_key betree.Message msgs1 key + if b + then + match new_msg with + | betree.Message.Insert i => + do + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, + betree.Message.Insert i) + lookup_first_message_for_key_back msgs3 + | betree.Message.Delete => + do + let msgs2 ← betree.Node.filter_messages_for_key key msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, + betree.Message.Delete) + lookup_first_message_for_key_back msgs3 + | 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 v ← betree.upsert_update (some prev) s + let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, + betree.Message.Insert v) + lookup_first_message_for_key_back msgs3 + | betree.Message.Delete => + do + let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 + let v ← betree.upsert_update none s + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, + betree.Message.Insert v) + lookup_first_message_for_key_back msgs3 + | betree.Message.Upsert _ => + do + let (msgs2, lookup_first_message_after_key_back) ← + betree.Node.lookup_first_message_after_key key msgs1 + let msgs3 ← + betree.List.push_front (U64 × betree.Message) msgs2 (key, + betree.Message.Upsert s) + let msgs4 ← lookup_first_message_after_key_back msgs3 + lookup_first_message_for_key_back msgs4 + else + do + let msgs2 ← + betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) + lookup_first_message_for_key_back msgs2 + +/- [betree::betree::{betree::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)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × betree.Message)) + := + match new_msgs with + | betree.List.Cons new_msg new_msgs_tl => + do + let (i, m) := new_msg + let msgs1 ← betree.Node.apply_to_internal msgs i m + betree.Node.apply_messages_to_internal msgs1 new_msgs_tl + | betree.List.Nil => Result.ok msgs + +/- [betree::betree::{betree::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)) × (betree.List (U64 × U64) → Result + (betree.List (U64 × U64)))) + := + match bindings with + | betree.List.Cons hd tl => + let (i, i1) := hd + if i >= key + then Result.ok (betree.List.Cons (i, i1) tl, Result.ok) + else + do + let (l, lookup_mut_in_bindings_back) ← + betree.Node.lookup_mut_in_bindings key tl + let back := + fun ret => + do + let tl1 ← lookup_mut_in_bindings_back ret + Result.ok (betree.List.Cons (i, i1) tl1) + Result.ok (l, back) + | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) + +/- [betree::betree::{betree::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) + : + Result (betree.List (U64 × U64)) + := + do + let (bindings1, lookup_mut_in_bindings_back) ← + betree.Node.lookup_mut_in_bindings key bindings + let b ← betree.ListPairU64T.head_has_key U64 bindings1 key + if b + then + do + let (hd, bindings2) ← betree.List.pop_front (U64 × U64) bindings1 + match new_msg with + | betree.Message.Insert v => + do + let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v) + lookup_mut_in_bindings_back bindings3 + | betree.Message.Delete => lookup_mut_in_bindings_back bindings2 + | betree.Message.Upsert s => + do + let (_, i) := hd + let v ← betree.upsert_update (some i) s + let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v) + lookup_mut_in_bindings_back bindings3 + else + match new_msg with + | betree.Message.Insert v => + do + let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back bindings2 + | betree.Message.Delete => lookup_mut_in_bindings_back bindings1 + | betree.Message.Upsert s => + do + let v ← betree.upsert_update none s + let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) + lookup_mut_in_bindings_back bindings2 + +/- [betree::betree::{betree::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)) + (new_msgs : betree.List (U64 × betree.Message)) : + Result (betree.List (U64 × U64)) + := + match new_msgs with + | betree.List.Cons new_msg new_msgs_tl => + do + let (i, m) := new_msg + let bindings1 ← betree.Node.apply_to_leaf bindings i m + betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl + | betree.List.Nil => Result.ok bindings + +/- [betree::betree::{betree::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)) × (betree.Internal + × betree.NodeIdCounter))) + := + do + let p ← + betree.ListPairU64T.partition_at_pivot betree.Message content self.pivot + 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 self.left params node_id_cnt msgs_left st + let (n, 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 (st2, p2) ← + betree.Node.apply_messages self.right params node_id_cnt1 msgs_right + st1 + let (n1, node_id_cnt2) := p2 + Result.ok (st2, (betree.List.Nil, (betree.Internal.mk self.id self.pivot + n n1, node_id_cnt2))) + else + Result.ok (st1, (msgs_right, (betree.Internal.mk self.id self.pivot n + self.right, node_id_cnt1))) + else + do + let (st1, p1) ← + betree.Node.apply_messages self.right params node_id_cnt msgs_right st + let (n, node_id_cnt1) := p1 + Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot + self.left n, node_id_cnt1))) + +/- [betree::betree::{betree::betree::Node#5}::apply_messages]: + 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 × (betree.Node × betree.NodeIdCounter)) + := + match self with + | betree.Node.Internal node => + do + let (st1, content) ← betree.load_internal_node node.id st + let content1 ← betree.Node.apply_messages_to_internal content msgs + let num_msgs ← betree.List.len (U64 × betree.Message) content1 + if num_msgs >= params.min_flush_size + then + do + let (st2, (content2, p)) ← + betree.Internal.flush node params node_id_cnt content1 st1 + let (node1, node_id_cnt1) := p + let (st3, _) ← betree.store_internal_node node1.id content2 st2 + Result.ok (st3, (betree.Node.Internal node1, node_id_cnt1)) + else + do + let (st2, _) ← betree.store_internal_node node.id content1 st1 + Result.ok (st2, (betree.Node.Internal node, node_id_cnt)) + | betree.Node.Leaf node => + do + let (st1, content) ← betree.load_leaf_node node.id st + let content1 ← betree.Node.apply_messages_to_leaf content msgs + let len ← betree.List.len (U64 × U64) content1 + let i ← 2#u64 * params.split_size + if len >= i + then + do + let (st2, (new_node, node_id_cnt1)) ← + betree.Leaf.split node content1 params node_id_cnt st1 + let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2 + Result.ok (st3, (betree.Node.Internal new_node, node_id_cnt1)) + else + do + let (st2, _) ← betree.store_leaf_node node.id content1 st1 + Result.ok (st2, (betree.Node.Leaf { node with size := len }, + node_id_cnt)) + +end + +/- [betree::betree::{betree::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 × (betree.Node × betree.NodeIdCounter)) + := + do + let (st1, p) ← + betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key, + new_msg) betree.List.Nil) st + let (self1, node_id_cnt1) := p + Result.ok (st1, (self1, node_id_cnt1)) + +/- [betree::betree::{betree::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, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt + let (st1, _) ← betree.store_leaf_node id betree.List.Nil st + Result.ok (st1, + { + params := { min_flush_size := min_flush_size, split_size := split_size }, + node_id_cnt := node_id_cnt1, + root := (betree.Node.Leaf { id := id, size := 0#u64 }) + }) + +/- [betree::betree::{betree::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 × betree.BeTree) + := + do + let (st1, p) ← + betree.Node.apply self.root self.params self.node_id_cnt key msg st + let (n, nic) := p + Result.ok (st1, { self with node_id_cnt := nic, root := n }) + +/- [betree::betree::{betree::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 × betree.BeTree) + := + betree.BeTree.apply self key (betree.Message.Insert value) st + +/- [betree::betree::{betree::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 × betree.BeTree) + := + betree.BeTree.apply self key betree.Message.Delete st + +/- [betree::betree::{betree::betree::BeTree#6}::upsert]: + 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 × betree.BeTree) + := + betree.BeTree.apply self key (betree.Message.Upsert upd) st + +/- [betree::betree::{betree::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) × betree.BeTree)) + := + do + let (st1, (o, n)) ← betree.Node.lookup self.root key st + Result.ok (st1, (o, { self with root := n })) + +/- [betree::main]: + Source: 'src/main.rs', lines 4:0-4:9 -/ +def main : Result Unit := + Result.ok () + +/- Unit test for [betree::main] -/ +#assert (main == Result.ok ()) + +end betree diff --git a/tests/lean/Betree/FunsExternal.lean b/tests/lean/Betree/FunsExternal.lean new file mode 100644 index 00000000..859cbd68 --- /dev/null +++ b/tests/lean/Betree/FunsExternal.lean @@ -0,0 +1,30 @@ +-- [betree]: external functions. +import Base +import Betree.Types +open Primitives +open betree + +-- TODO: fill those bodies + +/- [betree::betree_utils::load_internal_node] -/ +def betree_utils.load_internal_node + : + U64 → State → Result (State × (betree.List (U64 × betree.Message))) := + fun _ _ => .fail .panic + +/- [betree::betree_utils::store_internal_node] -/ +def betree_utils.store_internal_node + : + U64 → betree.List (U64 × betree.Message) → State → Result (State + × Unit) := + fun _ _ _ => .fail .panic + +/- [betree::betree_utils::load_leaf_node] -/ +def betree_utils.load_leaf_node + : U64 → State → Result (State × (betree.List (U64 × U64))) := + fun _ _ => .fail .panic + +/- [betree::betree_utils::store_leaf_node] -/ +def betree_utils.store_leaf_node + : U64 → betree.List (U64 × U64) → State → Result (State × Unit) := + fun _ _ _ => .fail .panic diff --git a/tests/lean/Betree/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean new file mode 100644 index 00000000..014f0d83 --- /dev/null +++ b/tests/lean/Betree/FunsExternal_Template.lean @@ -0,0 +1,30 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. +import Base +import Betree.Types +open Primitives +open betree + +/- [betree::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::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::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::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) + diff --git a/tests/lean/Betree/Types.lean b/tests/lean/Betree/Types.lean new file mode 100644 index 00000000..3b46c00c --- /dev/null +++ b/tests/lean/Betree/Types.lean @@ -0,0 +1,83 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree]: type definitions +import Base +import Betree.TypesExternal +open Primitives + +namespace betree + +/- [betree::betree::List] + Source: 'src/betree.rs', lines 17:0-17:23 -/ +inductive betree.List (T : Type) := +| Cons : T → betree.List T → betree.List T +| Nil : betree.List T + +/- [betree::betree::UpsertFunState] + Source: 'src/betree.rs', lines 63:0-63:23 -/ +inductive betree.UpsertFunState := +| Add : U64 → betree.UpsertFunState +| Sub : U64 → betree.UpsertFunState + +/- [betree::betree::Message] + Source: 'src/betree.rs', lines 69:0-69:23 -/ +inductive betree.Message := +| Insert : U64 → betree.Message +| Delete : betree.Message +| Upsert : betree.UpsertFunState → betree.Message + +/- [betree::betree::Leaf] + Source: 'src/betree.rs', lines 167:0-167:11 -/ +structure betree.Leaf where + id : U64 + size : U64 + +mutual + +/- [betree::betree::Internal] + Source: 'src/betree.rs', lines 156:0-156:15 -/ +inductive betree.Internal := +| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal + +/- [betree::betree::Node] + Source: 'src/betree.rs', lines 179:0-179:9 -/ +inductive betree.Node := +| Internal : betree.Internal → betree.Node +| Leaf : betree.Leaf → betree.Node + +end + +@[simp, reducible] +def betree.Internal.id (x : betree.Internal) := + match x with | betree.Internal.mk x1 _ _ _ => x1 + +@[simp, reducible] +def betree.Internal.pivot (x : betree.Internal) := + match x with | betree.Internal.mk _ x1 _ _ => x1 + +@[simp, reducible] +def betree.Internal.left (x : betree.Internal) := + match x with | betree.Internal.mk _ _ x1 _ => x1 + +@[simp, reducible] +def betree.Internal.right (x : betree.Internal) := + match x with | betree.Internal.mk _ _ _ x1 => x1 + +/- [betree::betree::Params] + Source: 'src/betree.rs', lines 187:0-187:13 -/ +structure betree.Params where + min_flush_size : U64 + split_size : U64 + +/- [betree::betree::NodeIdCounter] + Source: 'src/betree.rs', lines 201:0-201:20 -/ +structure betree.NodeIdCounter where + next_node_id : U64 + +/- [betree::betree::BeTree] + Source: 'src/betree.rs', lines 218:0-218:17 -/ +structure betree.BeTree where + params : betree.Params + node_id_cnt : betree.NodeIdCounter + root : betree.Node + +end betree diff --git a/tests/lean/Betree/TypesExternal.lean b/tests/lean/Betree/TypesExternal.lean new file mode 100644 index 00000000..34170271 --- /dev/null +++ b/tests/lean/Betree/TypesExternal.lean @@ -0,0 +1,7 @@ +-- [betree]: external types. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/Betree/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean new file mode 100644 index 00000000..12fce657 --- /dev/null +++ b/tests/lean/Betree/TypesExternal_Template.lean @@ -0,0 +1,9 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/BetreeMain.lean b/tests/lean/BetreeMain.lean deleted file mode 100644 index 5f307877..00000000 --- a/tests/lean/BetreeMain.lean +++ /dev/null @@ -1 +0,0 @@ -import BetreeMain.Funs diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean deleted file mode 100644 index f6fda6db..00000000 --- a/tests/lean/BetreeMain/Funs.lean +++ /dev/null @@ -1,699 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: function definitions -import Base -import BetreeMain.Types -import BetreeMain.FunsExternal -open Primitives - -namespace betree_main - -/- [betree_main::betree::load_internal_node]: - Source: 'src/betree.rs', lines 36:0-36:52 -/ -def betree.load_internal_node - (id : U64) (st : State) : - Result (State × (betree.List (U64 × betree.Message))) - := - betree_utils.load_internal_node id st - -/- [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) - := - betree_utils.store_internal_node id content st - -/- [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]: - 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) - := - betree_utils.store_leaf_node id content st - -/- [betree_main::betree::fresh_node_id]: - Source: 'src/betree.rs', lines 55:0-55:48 -/ -def betree.fresh_node_id (counter : U64) : Result (U64 × U64) := - do - let counter1 ← counter + 1#u64 - Result.ok (counter, counter1) - -/- [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.ok { next_node_id := 0#u64 } - -/- [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 × betree.NodeIdCounter) := - do - let i ← self.next_node_id + 1#u64 - Result.ok (self.next_node_id, { next_node_id := i }) - -/- [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 := - match prev with - | none => - match st with - | betree.UpsertFunState.Add v => Result.ok v - | betree.UpsertFunState.Sub _ => Result.ok 0#u64 - | some prev1 => - match st with - | betree.UpsertFunState.Add v => - do - let margin ← core_u64_max - prev1 - if margin >= v - then prev1 + v - else Result.ok core_u64_max - | betree.UpsertFunState.Sub v => - if prev1 >= v - then prev1 - v - else Result.ok 0#u64 - -/- [betree_main::betree::{betree_main::betree::List#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 _ tl => do - let i ← betree.List.len T tl - 1#u64 + i - | betree.List.Nil => Result.ok 0#u64 - -/- [betree_main::betree::{betree_main::betree::List#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) : - Result ((betree.List T) × (betree.List T)) - := - if n = 0#u64 - then Result.ok (betree.List.Nil, self) - else - 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 - Result.ok (betree.List.Cons hd ls0, ls1) - | betree.List.Nil => Result.fail .panic - -/- [betree_main::betree::{betree_main::betree::List#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 - Result.ok (betree.List.Cons x tl) - -/- [betree_main::betree::{betree_main::betree::List#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 -/ -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.ok (x, tl) - | betree.List.Nil => Result.fail .panic - -/- [betree_main::betree::{betree_main::betree::List#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 _ => Result.ok hd - | betree.List.Nil => Result.fail .panic - -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 -/ -def betree.ListPairU64T.head_has_key - (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool := - match self with - | betree.List.Cons hd _ => let (i, _) := hd - Result.ok (i = key) - | betree.List.Nil => Result.ok false - -/- [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.ListPairU64T.partition_at_pivot - (T : Type) (self : betree.List (U64 × T)) (pivot : U64) : - Result ((betree.List (U64 × T)) × (betree.List (U64 × T))) - := - match self with - | betree.List.Cons hd tl => - let (i, t) := hd - if i >= pivot - then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl) - else - do - let p ← betree.ListPairU64T.partition_at_pivot T tl pivot - let (ls0, ls1) := p - Result.ok (betree.List.Cons (i, t) ls0, ls1) - | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil) - -/- [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 × betree.NodeIdCounter)) - := - do - 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, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt - let (id1, node_id_cnt2) ← betree.NodeIdCounter.fresh_id node_id_cnt1 - 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.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2)) - -/- [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)) × (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.ok (betree.List.Cons (i, m) next_msgs, Result.ok) - else - do - let (l, lookup_first_message_for_key_back) ← - betree.Node.lookup_first_message_for_key key next_msgs - let back := - fun ret => - do - let next_msgs1 ← lookup_first_message_for_key_back ret - Result.ok (betree.List.Cons (i, m) next_msgs1) - Result.ok (l, back) - | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) - -/- [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, i1) := hd - if i = key - then Result.ok (some i1) - else - if i > key - then Result.ok none - else betree.Node.lookup_in_bindings key tl - | betree.List.Nil => Result.ok none - -/- [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) - : - Result (U64 × (betree.List (U64 × betree.Message))) - := - do - let b ← betree.ListPairU64T.head_has_key betree.Message msgs key - if b - then - do - let (msg, msgs1) ← 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 ← betree.upsert_update prev s - betree.Node.apply_upserts msgs1 (some v) key - else - do - let v ← core.option.Option.unwrap U64 prev - let msgs1 ← - betree.List.push_front (U64 × betree.Message) msgs (key, - betree.Message.Insert v) - Result.ok (v, msgs1) - -/- [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) × betree.Internal)) - := - if key < self.pivot - then - do - let (st1, (o, n)) ← betree.Node.lookup self.left key st - Result.ok (st1, (o, betree.Internal.mk self.id self.pivot n self.right)) - else - do - let (st1, (o, n)) ← betree.Node.lookup self.right key st - Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n)) - -/- [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) × betree.Node)) - := - match self with - | betree.Node.Internal node => - do - let (st1, msgs) ← betree.load_internal_node node.id 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 (st2, (o, node1)) ← - betree.Internal.lookup_in_children node key st1 - let _ ← - lookup_first_message_for_key_back (betree.List.Cons (k, msg) l) - Result.ok (st2, (o, betree.Node.Internal node1)) - else - match msg with - | betree.Message.Insert v => - do - let _ ← - lookup_first_message_for_key_back (betree.List.Cons (k, - betree.Message.Insert v) l) - Result.ok (st1, (some v, betree.Node.Internal node)) - | betree.Message.Delete => - do - let _ ← - lookup_first_message_for_key_back (betree.List.Cons (k, - betree.Message.Delete) l) - Result.ok (st1, (none, betree.Node.Internal node)) - | betree.Message.Upsert ufs => - do - let (st2, (v, node1)) ← - betree.Internal.lookup_in_children node key st1 - let (v1, pending1) ← - betree.Node.apply_upserts (betree.List.Cons (k, - betree.Message.Upsert ufs) l) v key - let msgs1 ← lookup_first_message_for_key_back pending1 - let (st3, _) ← betree.store_internal_node node1.id msgs1 st2 - Result.ok (st3, (some v1, betree.Node.Internal node1)) - | betree.List.Nil => - do - let (st2, (o, node1)) ← betree.Internal.lookup_in_children node key st1 - let _ ← lookup_first_message_for_key_back betree.List.Nil - Result.ok (st2, (o, betree.Node.Internal node1)) - | betree.Node.Leaf node => - do - let (st1, bindings) ← betree.load_leaf_node node.id st - let o ← betree.Node.lookup_in_bindings key bindings - Result.ok (st1, (o, betree.Node.Leaf node)) - -end - -/- [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)) : - Result (betree.List (U64 × betree.Message)) - := - match msgs with - | betree.List.Cons p l => - let (k, m) := p - if k = key - then - do - let (_, msgs1) ← - betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m) - l) - betree.Node.filter_messages_for_key key msgs1 - else Result.ok (betree.List.Cons (k, m) l) - | betree.List.Nil => Result.ok betree.List.Nil - -/- [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)) × (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 - do - let (l, lookup_first_message_after_key_back) ← - betree.Node.lookup_first_message_after_key key next_msgs - let back := - fun ret => - do - let next_msgs1 ← lookup_first_message_after_key_back ret - Result.ok (betree.List.Cons (k, m) next_msgs1) - Result.ok (l, back) - else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok) - | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) - -/- [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) - (new_msg : betree.Message) : - Result (betree.List (U64 × betree.Message)) - := - do - let (msgs1, lookup_first_message_for_key_back) ← - betree.Node.lookup_first_message_for_key key msgs - let b ← betree.ListPairU64T.head_has_key betree.Message msgs1 key - if b - then - match new_msg with - | betree.Message.Insert i => - do - let msgs2 ← betree.Node.filter_messages_for_key key msgs1 - let msgs3 ← - betree.List.push_front (U64 × betree.Message) msgs2 (key, - betree.Message.Insert i) - lookup_first_message_for_key_back msgs3 - | betree.Message.Delete => - do - let msgs2 ← betree.Node.filter_messages_for_key key msgs1 - let msgs3 ← - betree.List.push_front (U64 × betree.Message) msgs2 (key, - betree.Message.Delete) - lookup_first_message_for_key_back msgs3 - | 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 v ← betree.upsert_update (some prev) s - let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 - let msgs3 ← - betree.List.push_front (U64 × betree.Message) msgs2 (key, - betree.Message.Insert v) - lookup_first_message_for_key_back msgs3 - | betree.Message.Delete => - do - let (_, msgs2) ← betree.List.pop_front (U64 × betree.Message) msgs1 - let v ← betree.upsert_update none s - let msgs3 ← - betree.List.push_front (U64 × betree.Message) msgs2 (key, - betree.Message.Insert v) - lookup_first_message_for_key_back msgs3 - | betree.Message.Upsert _ => - do - let (msgs2, lookup_first_message_after_key_back) ← - betree.Node.lookup_first_message_after_key key msgs1 - let msgs3 ← - betree.List.push_front (U64 × betree.Message) msgs2 (key, - betree.Message.Upsert s) - let msgs4 ← lookup_first_message_after_key_back msgs3 - lookup_first_message_for_key_back msgs4 - else - do - let msgs2 ← - betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg) - lookup_first_message_for_key_back msgs2 - -/- [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)) - (new_msgs : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × betree.Message)) - := - match new_msgs with - | betree.List.Cons new_msg new_msgs_tl => - do - let (i, m) := new_msg - let msgs1 ← betree.Node.apply_to_internal msgs i m - betree.Node.apply_messages_to_internal msgs1 new_msgs_tl - | betree.List.Nil => Result.ok msgs - -/- [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)) × (betree.List (U64 × U64) → Result - (betree.List (U64 × U64)))) - := - match bindings with - | betree.List.Cons hd tl => - let (i, i1) := hd - if i >= key - then Result.ok (betree.List.Cons (i, i1) tl, Result.ok) - else - do - let (l, lookup_mut_in_bindings_back) ← - betree.Node.lookup_mut_in_bindings key tl - let back := - fun ret => - do - let tl1 ← lookup_mut_in_bindings_back ret - Result.ok (betree.List.Cons (i, i1) tl1) - Result.ok (l, back) - | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok) - -/- [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) - : - Result (betree.List (U64 × U64)) - := - do - let (bindings1, lookup_mut_in_bindings_back) ← - betree.Node.lookup_mut_in_bindings key bindings - let b ← betree.ListPairU64T.head_has_key U64 bindings1 key - if b - then - do - let (hd, bindings2) ← betree.List.pop_front (U64 × U64) bindings1 - match new_msg with - | betree.Message.Insert v => - do - let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v) - lookup_mut_in_bindings_back bindings3 - | betree.Message.Delete => lookup_mut_in_bindings_back bindings2 - | betree.Message.Upsert s => - do - let (_, i) := hd - let v ← betree.upsert_update (some i) s - let bindings3 ← betree.List.push_front (U64 × U64) bindings2 (key, v) - lookup_mut_in_bindings_back bindings3 - else - match new_msg with - | betree.Message.Insert v => - do - let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) - lookup_mut_in_bindings_back bindings2 - | betree.Message.Delete => lookup_mut_in_bindings_back bindings1 - | betree.Message.Upsert s => - do - let v ← betree.upsert_update none s - let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v) - lookup_mut_in_bindings_back bindings2 - -/- [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)) - (new_msgs : betree.List (U64 × betree.Message)) : - Result (betree.List (U64 × U64)) - := - match new_msgs with - | betree.List.Cons new_msg new_msgs_tl => - do - let (i, m) := new_msg - let bindings1 ← betree.Node.apply_to_leaf bindings i m - betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl - | betree.List.Nil => Result.ok bindings - -/- [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)) × (betree.Internal - × betree.NodeIdCounter))) - := - do - let p ← - betree.ListPairU64T.partition_at_pivot betree.Message content self.pivot - 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 self.left params node_id_cnt msgs_left st - let (n, 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 (st2, p2) ← - betree.Node.apply_messages self.right params node_id_cnt1 msgs_right - st1 - let (n1, node_id_cnt2) := p2 - Result.ok (st2, (betree.List.Nil, (betree.Internal.mk self.id self.pivot - n n1, node_id_cnt2))) - else - Result.ok (st1, (msgs_right, (betree.Internal.mk self.id self.pivot n - self.right, node_id_cnt1))) - else - do - let (st1, p1) ← - betree.Node.apply_messages self.right params node_id_cnt msgs_right st - let (n, node_id_cnt1) := p1 - Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot - self.left n, node_id_cnt1))) - -/- [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 - (self : betree.Node) (params : betree.Params) - (node_id_cnt : betree.NodeIdCounter) - (msgs : betree.List (U64 × betree.Message)) (st : State) : - Result (State × (betree.Node × betree.NodeIdCounter)) - := - match self with - | betree.Node.Internal node => - do - let (st1, content) ← betree.load_internal_node node.id st - let content1 ← betree.Node.apply_messages_to_internal content msgs - let num_msgs ← betree.List.len (U64 × betree.Message) content1 - if num_msgs >= params.min_flush_size - then - do - let (st2, (content2, p)) ← - betree.Internal.flush node params node_id_cnt content1 st1 - let (node1, node_id_cnt1) := p - let (st3, _) ← betree.store_internal_node node1.id content2 st2 - Result.ok (st3, (betree.Node.Internal node1, node_id_cnt1)) - else - do - let (st2, _) ← betree.store_internal_node node.id content1 st1 - Result.ok (st2, (betree.Node.Internal node, node_id_cnt)) - | betree.Node.Leaf node => - do - let (st1, content) ← betree.load_leaf_node node.id st - let content1 ← betree.Node.apply_messages_to_leaf content msgs - let len ← betree.List.len (U64 × U64) content1 - let i ← 2#u64 * params.split_size - if len >= i - then - do - let (st2, (new_node, node_id_cnt1)) ← - betree.Leaf.split node content1 params node_id_cnt st1 - let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2 - Result.ok (st3, (betree.Node.Internal new_node, node_id_cnt1)) - else - do - let (st2, _) ← betree.store_leaf_node node.id content1 st1 - Result.ok (st2, (betree.Node.Leaf { node with size := len }, - node_id_cnt)) - -end - -/- [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 × (betree.Node × betree.NodeIdCounter)) - := - do - let (st1, p) ← - betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key, - new_msg) betree.List.Nil) st - let (self1, node_id_cnt1) := p - Result.ok (st1, (self1, node_id_cnt1)) - -/- [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, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt - let (st1, _) ← betree.store_leaf_node id betree.List.Nil st - Result.ok (st1, - { - params := { min_flush_size := min_flush_size, split_size := split_size }, - node_id_cnt := node_id_cnt1, - 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 × betree.BeTree) - := - do - let (st1, p) ← - betree.Node.apply self.root self.params self.node_id_cnt key msg st - let (n, nic) := p - Result.ok (st1, { self with node_id_cnt := nic, root := n }) - -/- [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 × betree.BeTree) - := - betree.BeTree.apply self key (betree.Message.Insert value) st - -/- [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 × betree.BeTree) - := - betree.BeTree.apply self key betree.Message.Delete st - -/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: - 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 × betree.BeTree) - := - betree.BeTree.apply self key (betree.Message.Upsert upd) st - -/- [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) × betree.BeTree)) - := - do - let (st1, (o, n)) ← betree.Node.lookup self.root key st - Result.ok (st1, (o, { self with root := n })) - -/- [betree_main::main]: - Source: 'src/main.rs', lines 4:0-4:9 -/ -def main : Result Unit := - Result.ok () - -/- Unit test for [betree_main::main] -/ -#assert (main == Result.ok ()) - -end betree_main diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/BetreeMain/FunsExternal.lean deleted file mode 100644 index d26177fb..00000000 --- a/tests/lean/BetreeMain/FunsExternal.lean +++ /dev/null @@ -1,30 +0,0 @@ --- [betree_main]: external functions. -import Base -import BetreeMain.Types -open Primitives -open betree_main - --- TODO: fill those bodies - -/- [betree_main::betree_utils::load_internal_node] -/ -def betree_utils.load_internal_node - : - U64 → State → Result (State × (betree.List (U64 × betree.Message))) := - fun _ _ => .fail .panic - -/- [betree_main::betree_utils::store_internal_node] -/ -def betree_utils.store_internal_node - : - U64 → betree.List (U64 × betree.Message) → State → Result (State - × Unit) := - fun _ _ _ => .fail .panic - -/- [betree_main::betree_utils::load_leaf_node] -/ -def betree_utils.load_leaf_node - : U64 → State → Result (State × (betree.List (U64 × U64))) := - fun _ _ => .fail .panic - -/- [betree_main::betree_utils::store_leaf_node] -/ -def betree_utils.store_leaf_node - : U64 → betree.List (U64 × U64) → State → Result (State × Unit) := - fun _ _ _ => .fail .panic diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean deleted file mode 100644 index 0dcce5ca..00000000 --- a/tests/lean/BetreeMain/FunsExternal_Template.lean +++ /dev/null @@ -1,30 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: external functions. --- This is a template file: rename it to "FunsExternal.lean" and fill the holes. -import Base -import BetreeMain.Types -open Primitives -open betree_main - -/- [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]: - 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]: - 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]: - 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) - diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean deleted file mode 100644 index e79da43f..00000000 --- a/tests/lean/BetreeMain/Types.lean +++ /dev/null @@ -1,83 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: type definitions -import Base -import BetreeMain.TypesExternal -open Primitives - -namespace betree_main - -/- [betree_main::betree::List] - Source: 'src/betree.rs', lines 17:0-17:23 -/ -inductive betree.List (T : Type) := -| Cons : T → betree.List T → betree.List T -| Nil : betree.List T - -/- [betree_main::betree::UpsertFunState] - Source: 'src/betree.rs', lines 63:0-63:23 -/ -inductive betree.UpsertFunState := -| Add : U64 → betree.UpsertFunState -| Sub : U64 → betree.UpsertFunState - -/- [betree_main::betree::Message] - Source: 'src/betree.rs', lines 69:0-69:23 -/ -inductive betree.Message := -| Insert : U64 → betree.Message -| Delete : betree.Message -| Upsert : betree.UpsertFunState → betree.Message - -/- [betree_main::betree::Leaf] - Source: 'src/betree.rs', lines 167:0-167:11 -/ -structure betree.Leaf where - id : U64 - size : U64 - -mutual - -/- [betree_main::betree::Internal] - Source: 'src/betree.rs', lines 156:0-156:15 -/ -inductive betree.Internal := -| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal - -/- [betree_main::betree::Node] - Source: 'src/betree.rs', lines 179:0-179:9 -/ -inductive betree.Node := -| Internal : betree.Internal → betree.Node -| Leaf : betree.Leaf → betree.Node - -end - -@[simp, reducible] -def betree.Internal.id (x : betree.Internal) := - match x with | betree.Internal.mk x1 _ _ _ => x1 - -@[simp, reducible] -def betree.Internal.pivot (x : betree.Internal) := - match x with | betree.Internal.mk _ x1 _ _ => x1 - -@[simp, reducible] -def betree.Internal.left (x : betree.Internal) := - match x with | betree.Internal.mk _ _ x1 _ => x1 - -@[simp, reducible] -def betree.Internal.right (x : betree.Internal) := - match x with | betree.Internal.mk _ _ _ x1 => x1 - -/- [betree_main::betree::Params] - Source: 'src/betree.rs', lines 187:0-187:13 -/ -structure betree.Params where - min_flush_size : U64 - split_size : U64 - -/- [betree_main::betree::NodeIdCounter] - Source: 'src/betree.rs', lines 201:0-201:20 -/ -structure betree.NodeIdCounter where - next_node_id : U64 - -/- [betree_main::betree::BeTree] - Source: 'src/betree.rs', lines 218:0-218:17 -/ -structure betree.BeTree where - params : betree.Params - node_id_cnt : betree.NodeIdCounter - root : betree.Node - -end betree_main diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/BetreeMain/TypesExternal.lean deleted file mode 100644 index 1701eaaf..00000000 --- a/tests/lean/BetreeMain/TypesExternal.lean +++ /dev/null @@ -1,7 +0,0 @@ --- [betree_main]: external types. -import Base -open Primitives - -/- The state type used in the state-error monad -/ -axiom State : Type - diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/BetreeMain/TypesExternal_Template.lean deleted file mode 100644 index bbac7e99..00000000 --- a/tests/lean/BetreeMain/TypesExternal_Template.lean +++ /dev/null @@ -1,9 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: external types. --- This is a template file: rename it to "TypesExternal.lean" and fill the holes. -import Base -open Primitives - -/- The state type used in the state-error monad -/ -axiom State : Type - diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index bb13ddf2..ba336a4a 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -9,7 +9,7 @@ require base from "../../backends/lean" package «tests» {} @[default_target] lean_lib Tutorial -@[default_target] lean_lib BetreeMain +@[default_target] lean_lib Betree @[default_target] lean_lib Constants @[default_target] lean_lib External @[default_target] lean_lib Hashmap -- cgit v1.2.3 From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 17:33:56 +0200 Subject: Add some tests --- tests/lean/Issue194RecursiveStructProjector.lean | 35 ++++++++++++++++++++++++ tests/lean/Matches.lean | 16 +++++++++++ 2 files changed, 51 insertions(+) create mode 100644 tests/lean/Issue194RecursiveStructProjector.lean create mode 100644 tests/lean/Matches.lean (limited to 'tests/lean') diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean new file mode 100644 index 00000000..4eb23934 --- /dev/null +++ b/tests/lean/Issue194RecursiveStructProjector.lean @@ -0,0 +1,35 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [issue_194_recursive_struct_projector] +import Base +open Primitives + +namespace issue_194_recursive_struct_projector + +/- [issue_194_recursive_struct_projector::AVLNode] + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 -/ +inductive AVLNode (T : Type) := +| mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T + +@[simp, reducible] +def AVLNode.value {T : Type} (x : AVLNode T) := + match x with | AVLNode.mk x1 _ _ => x1 + +@[simp, reducible] +def AVLNode.left {T : Type} (x : AVLNode T) := + match x with | AVLNode.mk _ x1 _ => x1 + +@[simp, reducible] +def AVLNode.right {T : Type} (x : AVLNode T) := + match x with | AVLNode.mk _ _ x1 => x1 + +/- [issue_194_recursive_struct_projector::get_val]: + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 -/ +def get_val (T : Type) (x : AVLNode T) : Result T := + Result.ok x.value + +/- [issue_194_recursive_struct_projector::get_left]: + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 -/ +def get_left (T : Type) (x : AVLNode T) : Result (Option (AVLNode T)) := + Result.ok x.left + +end issue_194_recursive_struct_projector diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean new file mode 100644 index 00000000..3e3a558b --- /dev/null +++ b/tests/lean/Matches.lean @@ -0,0 +1,16 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [matches] +import Base +open Primitives + +namespace matches + +/- [matches::match_u32]: + Source: 'tests/src/matches.rs', lines 4:0-4:27 -/ +def match_u32 (x : U32) : Result U32 := + match x with + | 0#u32 => Result.ok 0#u32 + | 1#u32 => Result.ok 1#u32 + | _ => Result.ok 2#u32 + +end matches -- cgit v1.2.3 From c4d2af051c18c4c81b1e57a45210c37c89c8330f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 11:18:35 +0200 Subject: tests: Rename hashmap_utils -> utils --- tests/lean/Hashmap/Funs.lean | 4 ++-- tests/lean/Hashmap/FunsExternal.lean | 8 ++++---- tests/lean/Hashmap/FunsExternal_Template.lean | 9 ++++----- 3 files changed, 10 insertions(+), 11 deletions(-) (limited to 'tests/lean') diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index e76912cc..d7ac3b05 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -386,9 +386,9 @@ def HashMap.remove def insert_on_disk (key : Usize) (value : U64) (st : State) : Result (State × Unit) := do - let (st1, hm) ← hashmap_utils.deserialize st + let (st1, hm) ← utils.deserialize st let hm1 ← HashMap.insert U64 hm key value - hashmap_utils.serialize hm1 st1 + utils.serialize hm1 st1 /- [hashmap::test1]: Source: 'tests/src/hashmap.rs', lines 350:0-350:10 -/ diff --git a/tests/lean/Hashmap/FunsExternal.lean b/tests/lean/Hashmap/FunsExternal.lean index 7454696b..329e5d82 100644 --- a/tests/lean/Hashmap/FunsExternal.lean +++ b/tests/lean/Hashmap/FunsExternal.lean @@ -6,14 +6,14 @@ open hashmap -- TODO: fill those bodies -/- [hashmap::hashmap_utils::deserialize]: +/- [hashmap::utils::deserialize]: Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/ -def hashmap_utils.deserialize +def utils.deserialize : State → Result (State × (HashMap U64)) := fun _ => .fail .panic -/- [hashmap::hashmap_utils::serialize]: +/- [hashmap::utils::serialize]: Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/ -def hashmap_utils.serialize +def utils.serialize : HashMap U64 → State → Result (State × Unit) := fun _ _ => .fail .panic diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean index 16b4b6af..2af57d10 100644 --- a/tests/lean/Hashmap/FunsExternal_Template.lean +++ b/tests/lean/Hashmap/FunsExternal_Template.lean @@ -6,12 +6,11 @@ import Hashmap.Types open Primitives open hashmap -/- [hashmap::hashmap_utils::deserialize]: +/- [hashmap::utils::deserialize]: Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/ -axiom hashmap_utils.deserialize : State → Result (State × (HashMap U64)) +axiom utils.deserialize : State → Result (State × (HashMap U64)) -/- [hashmap::hashmap_utils::serialize]: +/- [hashmap::utils::serialize]: Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/ -axiom hashmap_utils.serialize - : HashMap U64 → State → Result (State × Unit) +axiom utils.serialize : HashMap U64 → State → Result (State × Unit) -- cgit v1.2.3