diff options
Diffstat (limited to 'tests/lean')
22 files changed, 205 insertions, 650 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/Betree/Funs.lean index f6fda6db..8612ccbc 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -1,13 +1,13 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: function definitions +-- [betree]: function definitions import Base -import BetreeMain.Types -import BetreeMain.FunsExternal +import Betree.Types +import Betree.FunsExternal open Primitives -namespace betree_main +namespace betree -/- [betree_main::betree::load_internal_node]: +/- [betree::betree::load_internal_node]: Source: 'src/betree.rs', lines 36:0-36:52 -/ def betree.load_internal_node (id : U64) (st : State) : @@ -15,7 +15,7 @@ def betree.load_internal_node := betree_utils.load_internal_node id st -/- [betree_main::betree::store_internal_node]: +/- [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) : @@ -23,13 +23,13 @@ def betree.store_internal_node := betree_utils.store_internal_node id content st -/- [betree_main::betree::load_leaf_node]: +/- [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_main::betree::store_leaf_node]: +/- [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) : @@ -37,19 +37,19 @@ def betree.store_leaf_node := betree_utils.store_leaf_node id content st -/- [betree_main::betree::fresh_node_id]: +/- [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_main::betree::{betree_main::betree::NodeIdCounter}::new]: +/- [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_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: +/- [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) := @@ -57,7 +57,7 @@ def betree.NodeIdCounter.fresh_id let i ← self.next_node_id + 1#u64 Result.ok (self.next_node_id, { next_node_id := i }) -/- [betree_main::betree::upsert_update]: +/- [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 := @@ -79,7 +79,7 @@ def betree.upsert_update then prev1 - v else Result.ok 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: +/- [betree::betree::{betree::betree::List<T>#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := match self with @@ -88,7 +88,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 := 1#u64 + i | betree.List.Nil => Result.ok 0#u64 -/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: +/- [betree::betree::{betree::betree::List<T>#1}::split_at]: Source: 'src/betree.rs', lines 284:4-284:51 -/ divergent def betree.List.split_at (T : Type) (self : betree.List T) (n : U64) : @@ -106,14 +106,14 @@ divergent def betree.List.split_at Result.ok (betree.List.Cons hd ls0, ls1) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: +/- [betree::betree::{betree::betree::List<T>#1}::push_front]: Source: 'src/betree.rs', lines 299:4-299:34 -/ def betree.List.push_front (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) := let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil Result.ok (betree.List.Cons x tl) -/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: +/- [betree::betree::{betree::betree::List<T>#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)) := @@ -122,14 +122,14 @@ def betree.List.pop_front | betree.List.Cons x tl => Result.ok (x, tl) | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: +/- [betree::betree::{betree::betree::List<T>#1}::hd]: Source: 'src/betree.rs', lines 318:4-318:22 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with | betree.List.Cons hd _ => Result.ok hd | betree.List.Nil => Result.fail .panic -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: +/- [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 := @@ -138,7 +138,7 @@ def betree.ListPairU64T.head_has_key Result.ok (i = key) | betree.List.Nil => Result.ok false -/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: +/- [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) : @@ -156,7 +156,7 @@ divergent def betree.ListPairU64T.partition_at_pivot 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]: +/- [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)) @@ -176,7 +176,7 @@ def betree.Leaf.split 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]: +/- [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)) : @@ -200,7 +200,7 @@ divergent def betree.Node.lookup_first_message_for_key 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]: +/- [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) := @@ -215,7 +215,7 @@ divergent def betree.Node.lookup_in_bindings else betree.Node.lookup_in_bindings key tl | betree.List.Nil => Result.ok none -/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: +/- [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) @@ -244,7 +244,7 @@ divergent def betree.Node.apply_upserts betree.Message.Insert v) Result.ok (v, msgs1) -/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: +/- [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) : @@ -260,7 +260,7 @@ mutual divergent def betree.Internal.lookup_in_children 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]: +/- [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) : @@ -320,7 +320,7 @@ divergent def betree.Node.lookup end -/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: +/- [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)) : @@ -339,7 +339,7 @@ divergent def betree.Node.filter_messages_for_key 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]: +/- [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)) : @@ -363,7 +363,7 @@ divergent def betree.Node.lookup_first_message_after_key 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]: +/- [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) @@ -427,7 +427,7 @@ def betree.Node.apply_to_internal 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]: +/- [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)) @@ -442,7 +442,7 @@ divergent def betree.Node.apply_messages_to_internal 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]: +/- [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)) : @@ -466,7 +466,7 @@ divergent def betree.Node.lookup_mut_in_bindings 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]: +/- [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) @@ -506,7 +506,7 @@ def betree.Node.apply_to_leaf 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]: +/- [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)) @@ -521,7 +521,7 @@ divergent def betree.Node.apply_messages_to_leaf 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]: +/- [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) @@ -562,7 +562,7 @@ mutual divergent def betree.Internal.flush 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]: +/- [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) @@ -609,7 +609,7 @@ divergent def betree.Node.apply_messages end -/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: +/- [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) @@ -624,7 +624,7 @@ def betree.Node.apply let (self1, node_id_cnt1) := p Result.ok (st1, (self1, node_id_cnt1)) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: +/- [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) : @@ -641,7 +641,7 @@ def betree.BeTree.new root := (betree.Node.Leaf { id := id, size := 0#u64 }) }) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: +/- [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) : @@ -653,7 +653,7 @@ def betree.BeTree.apply let (n, nic) := p Result.ok (st1, { self with node_id_cnt := nic, root := n }) -/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: +/- [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) : @@ -661,7 +661,7 @@ def betree.BeTree.insert := betree.BeTree.apply self key (betree.Message.Insert value) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: +/- [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) : @@ -669,7 +669,7 @@ def betree.BeTree.delete := betree.BeTree.apply self key betree.Message.Delete st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: +/- [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) @@ -678,7 +678,7 @@ def betree.BeTree.upsert := betree.BeTree.apply self key (betree.Message.Upsert upd) st -/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: +/- [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) : @@ -688,12 +688,12 @@ def betree.BeTree.lookup let (st1, (o, n)) ← betree.Node.lookup self.root key st Result.ok (st1, (o, { self with root := n })) -/- [betree_main::main]: +/- [betree::main]: Source: 'src/main.rs', lines 4:0-4:9 -/ def main : Result Unit := Result.ok () -/- Unit test for [betree_main::main] -/ +/- Unit test for [betree::main] -/ #assert (main == Result.ok ()) -end betree_main +end betree diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/Betree/FunsExternal.lean index d26177fb..859cbd68 100644 --- a/tests/lean/BetreeMain/FunsExternal.lean +++ b/tests/lean/Betree/FunsExternal.lean @@ -1,30 +1,30 @@ --- [betree_main]: external functions. +-- [betree]: external functions. import Base -import BetreeMain.Types +import Betree.Types open Primitives -open betree_main +open betree -- TODO: fill those bodies -/- [betree_main::betree_utils::load_internal_node] -/ +/- [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_main::betree_utils::store_internal_node] -/ +/- [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_main::betree_utils::load_leaf_node] -/ +/- [betree::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] -/ +/- [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/BetreeMain/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean index 0dcce5ca..014f0d83 100644 --- a/tests/lean/BetreeMain/FunsExternal_Template.lean +++ b/tests/lean/Betree/FunsExternal_Template.lean @@ -1,29 +1,29 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: external functions. +-- [betree]: external functions. -- This is a template file: rename it to "FunsExternal.lean" and fill the holes. import Base -import BetreeMain.Types +import Betree.Types open Primitives -open betree_main +open betree -/- [betree_main::betree_utils::load_internal_node]: +/- [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_main::betree_utils::store_internal_node]: +/- [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_main::betree_utils::load_leaf_node]: +/- [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_main::betree_utils::store_leaf_node]: +/- [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/BetreeMain/Types.lean b/tests/lean/Betree/Types.lean index e79da43f..3b46c00c 100644 --- a/tests/lean/BetreeMain/Types.lean +++ b/tests/lean/Betree/Types.lean @@ -1,31 +1,31 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: type definitions +-- [betree]: type definitions import Base -import BetreeMain.TypesExternal +import Betree.TypesExternal open Primitives -namespace betree_main +namespace betree -/- [betree_main::betree::List] +/- [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_main::betree::UpsertFunState] +/- [betree::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] +/- [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_main::betree::Leaf] +/- [betree::betree::Leaf] Source: 'src/betree.rs', lines 167:0-167:11 -/ structure betree.Leaf where id : U64 @@ -33,12 +33,12 @@ structure betree.Leaf where mutual -/- [betree_main::betree::Internal] +/- [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_main::betree::Node] +/- [betree::betree::Node] Source: 'src/betree.rs', lines 179:0-179:9 -/ inductive betree.Node := | Internal : betree.Internal → betree.Node @@ -62,22 +62,22 @@ def betree.Internal.left (x : betree.Internal) := def betree.Internal.right (x : betree.Internal) := match x with | betree.Internal.mk _ _ _ x1 => x1 -/- [betree_main::betree::Params] +/- [betree::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] +/- [betree::betree::NodeIdCounter] Source: 'src/betree.rs', lines 201:0-201:20 -/ structure betree.NodeIdCounter where next_node_id : U64 -/- [betree_main::betree::BeTree] +/- [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_main +end betree diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/Betree/TypesExternal.lean index 1701eaaf..34170271 100644 --- a/tests/lean/BetreeMain/TypesExternal.lean +++ b/tests/lean/Betree/TypesExternal.lean @@ -1,4 +1,4 @@ --- [betree_main]: external types. +-- [betree]: external types. import Base open Primitives diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean index bbac7e99..12fce657 100644 --- a/tests/lean/BetreeMain/TypesExternal_Template.lean +++ b/tests/lean/Betree/TypesExternal_Template.lean @@ -1,5 +1,5 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [betree_main]: external types. +-- [betree]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives 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/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 4f05fbc8..d7ac3b05 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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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) ← utils.deserialize st + let hm1 ← HashMap.insert U64 hm key value + 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..329e5d82 --- /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::utils::deserialize]: + Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/ +def utils.deserialize + : State → Result (State × (HashMap U64)) := + fun _ => .fail .panic + +/- [hashmap::utils::serialize]: + Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/ +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 new file mode 100644 index 00000000..2af57d10 --- /dev/null +++ b/tests/lean/Hashmap/FunsExternal_Template.lean @@ -0,0 +1,16 @@ +-- 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::utils::deserialize]: + Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/ +axiom utils.deserialize : State → Result (State × (HashMap U64)) + +/- [hashmap::utils::serialize]: + Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/ +axiom 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/HashmapMain/TypesExternal.lean b/tests/lean/Hashmap/TypesExternal.lean index 4e1cdbe9..b32c4c42 100644 --- a/tests/lean/HashmapMain/TypesExternal.lean +++ b/tests/lean/Hashmap/TypesExternal.lean @@ -1,4 +1,4 @@ --- [hashmap_main]: external types. +-- [hashmap]: external types. import Base open Primitives diff --git a/tests/lean/HashmapMain/TypesExternal_Template.lean b/tests/lean/Hashmap/TypesExternal_Template.lean index cfa8bbb1..03c3d157 100644 --- a/tests/lean/HashmapMain/TypesExternal_Template.lean +++ b/tests/lean/Hashmap/TypesExternal_Template.lean @@ -1,5 +1,5 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [hashmap_main]: external types. +-- [hashmap]: external types. -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives 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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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<T>}::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/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 diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean index 3a777824..ba336a4a 100644 --- a/tests/lean/lakefile.lean +++ b/tests/lean/lakefile.lean @@ -9,11 +9,10 @@ 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 -@[default_target] lean_lib HashmapMain @[default_target] lean_lib Loops @[default_target] lean_lib NoNestedBorrows @[default_target] lean_lib Paper |