From 4a34537a7fe33fa33d618b153832f9e750276480 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 14 Jun 2024 10:41:06 +0200 Subject: Update the code of the hashmap --- tests/src/hashmap.rs | 61 ++++++++++++++++++++++++++-------------------------- 1 file changed, 31 insertions(+), 30 deletions(-) (limited to 'tests/src') diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs index 7dda2404..9ff448db 100644 --- a/tests/src/hashmap.rs +++ b/tests/src/hashmap.rs @@ -26,8 +26,9 @@ use std::vec::Vec; pub type Key = usize; // TODO: make this generic pub type Hash = usize; -pub enum List { - Cons(Key, T, Box>), +/// Associative list +pub enum AList { + Cons(Key, T, Box>), Nil, } @@ -51,15 +52,15 @@ pub struct HashMap { /// gives the threshold at which to resize the table. max_load: usize, /// The table itself - slots: Vec>, + slots: Vec>, } impl HashMap { /// Allocate a vector of slots of a given size. /// We would need a loop, but can't use loops for now... - fn allocate_slots(mut slots: Vec>, mut n: usize) -> Vec> { + fn allocate_slots(mut slots: Vec>, mut n: usize) -> Vec> { while n > 0 { - slots.push(List::Nil); + slots.push(AList::Nil); n -= 1; } slots @@ -92,7 +93,7 @@ impl HashMap { let slots = &mut self.slots; let mut i = 0; while i < slots.len() { - slots[i] = List::Nil; + slots[i] = AList::Nil; i += 1; } } @@ -104,14 +105,14 @@ impl HashMap { /// Insert in a list. /// Return `true` if we inserted an element, `false` if we simply updated /// a value. - fn insert_in_list(key: Key, value: T, mut ls: &mut List) -> bool { + fn insert_in_list(key: Key, value: T, mut ls: &mut AList) -> bool { loop { match ls { - List::Nil => { - *ls = List::Cons(key, value, Box::new(List::Nil)); + AList::Nil => { + *ls = AList::Cons(key, value, Box::new(AList::Nil)); return true; } - List::Cons(ckey, cvalue, tl) => { + AList::Cons(ckey, cvalue, tl) => { if *ckey == key { *cvalue = value; return false; @@ -178,10 +179,10 @@ impl HashMap { /// Auxiliary function called by [try_resize] to move all the elements /// from the table to a new table - fn move_elements<'a>(ntable: &'a mut HashMap, slots: &'a mut Vec>, mut i: usize) { + fn move_elements<'a>(ntable: &'a mut HashMap, slots: &'a mut Vec>, mut i: usize) { while i < slots.len() { // Move the elements out of the slot i - let ls = std::mem::replace(&mut slots[i], List::Nil); + let ls = std::mem::replace(&mut slots[i], AList::Nil); // Move all those elements to the new table HashMap::move_elements_from_list(ntable, ls); // Do the same for slot i+1 @@ -190,12 +191,12 @@ impl HashMap { } /// Auxiliary function. - fn move_elements_from_list(ntable: &mut HashMap, mut ls: List) { + fn move_elements_from_list(ntable: &mut HashMap, mut ls: AList) { // As long as there are elements in the list, move them loop { match ls { - List::Nil => return, // We're done - List::Cons(k, v, tl) => { + AList::Nil => return, // We're done + AList::Cons(k, v, tl) => { // Insert the element in the new table ntable.insert_no_resize(k, v); // Move the elements out of the tail @@ -213,11 +214,11 @@ impl HashMap { } /// Returns `true` if the list contains a value for the specified key. - pub fn contains_key_in_list(key: &Key, mut ls: &List) -> bool { + pub fn contains_key_in_list(key: &Key, mut ls: &AList) -> bool { loop { match ls { - List::Nil => return false, - List::Cons(ckey, _, tl) => { + AList::Nil => return false, + AList::Cons(ckey, _, tl) => { if *ckey == *key { return true; } else { @@ -231,11 +232,11 @@ impl HashMap { /// We don't support borrows inside of enumerations for now, so we /// can't return an option... /// TODO: add support for that - fn get_in_list<'a, 'k>(key: &'k Key, mut ls: &'a List) -> &'a T { + fn get_in_list<'a, 'k>(key: &'k Key, mut ls: &'a AList) -> &'a T { loop { match ls { - List::Nil => panic!(), - List::Cons(ckey, cvalue, tl) => { + AList::Nil => panic!(), + AList::Cons(ckey, cvalue, tl) => { if *ckey == *key { return cvalue; } else { @@ -252,8 +253,8 @@ impl HashMap { HashMap::get_in_list(key, &self.slots[hash_mod]) } - pub fn get_mut_in_list<'a, 'k>(mut ls: &'a mut List, key: &'k Key) -> &'a mut T { - while let List::Cons(ckey, cvalue, tl) = ls { + pub fn get_mut_in_list<'a, 'k>(mut ls: &'a mut AList, key: &'k Key) -> &'a mut T { + while let AList::Cons(ckey, cvalue, tl) = ls { if *ckey == *key { return cvalue; } else { @@ -272,20 +273,20 @@ impl HashMap { /// Remove an element from the list. /// Return the removed element. - fn remove_from_list(key: &Key, mut ls: &mut List) -> Option { + fn remove_from_list(key: &Key, mut ls: &mut AList) -> Option { loop { match ls { - List::Nil => return None, + AList::Nil => return None, // We have to use a guard and split the Cons case into two // branches, otherwise the borrow checker is not happy. - List::Cons(ckey, _, _) if *ckey == *key => { + AList::Cons(ckey, _, _) if *ckey == *key => { // We have to move under borrows, so we need to use // [std::mem::replace] in several steps. // Retrieve the tail - let mv_ls = std::mem::replace(ls, List::Nil); + let mv_ls = std::mem::replace(ls, AList::Nil); match mv_ls { - List::Nil => unreachable!(), - List::Cons(_, cvalue, tl) => { + AList::Nil => unreachable!(), + AList::Cons(_, cvalue, tl) => { // Make the list equal to its tail *ls = *tl; // Return the dropped value @@ -293,7 +294,7 @@ impl HashMap { } } } - List::Cons(_, _, tl) => { + AList::Cons(_, _, tl) => { ls = tl; } } -- cgit v1.3.1 From cf7cd476b32cd562ca90950e4b3c29c9fc42028a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 17 Jun 2024 07:25:17 +0200 Subject: Regenerate the tests --- tests/lean/Arrays.lean | 3 +++ tests/lean/Betree/Funs.lean | 3 +++ tests/lean/Betree/FunsExternal_Template.lean | 3 +++ tests/lean/Betree/Types.lean | 3 +++ tests/lean/Betree/TypesExternal_Template.lean | 3 +++ tests/lean/Bitwise.lean | 3 +++ tests/lean/Constants.lean | 3 +++ tests/lean/Demo/Demo.lean | 3 +++ tests/lean/External/Funs.lean | 3 +++ tests/lean/External/FunsExternal_Template.lean | 3 +++ tests/lean/External/Types.lean | 3 +++ tests/lean/External/TypesExternal_Template.lean | 3 +++ tests/lean/Hashmap/Funs.lean | 3 +++ tests/lean/Hashmap/FunsExternal_Template.lean | 3 +++ tests/lean/Hashmap/Types.lean | 3 +++ tests/lean/Hashmap/TypesExternal_Template.lean | 3 +++ tests/lean/InfiniteLoop.lean | 3 +++ tests/lean/Issue194RecursiveStructProjector.lean | 3 +++ tests/lean/Loops.lean | 3 +++ tests/lean/Matches.lean | 3 +++ tests/lean/NoNestedBorrows.lean | 3 +++ tests/lean/Paper.lean | 3 +++ tests/lean/PoloniusList.lean | 3 +++ tests/lean/Traits.lean | 3 +++ tests/lean/misc/MutuallyRecursiveTraits.lean | 3 +++ tests/src/mutually-recursive-traits.lean.out | 4 ++-- 26 files changed, 77 insertions(+), 2 deletions(-) (limited to 'tests/src') diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 9748919e..bb97d5c4 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -2,6 +2,9 @@ -- [arrays] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace arrays diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 05341b31..4592e91c 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -4,6 +4,9 @@ import Base import Betree.Types import Betree.FunsExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace betree diff --git a/tests/lean/Betree/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean index 014f0d83..2fb40ebc 100644 --- a/tests/lean/Betree/FunsExternal_Template.lean +++ b/tests/lean/Betree/FunsExternal_Template.lean @@ -4,6 +4,9 @@ import Base import Betree.Types open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false open betree /- [betree::betree_utils::load_internal_node]: diff --git a/tests/lean/Betree/Types.lean b/tests/lean/Betree/Types.lean index 3b46c00c..9e7c505b 100644 --- a/tests/lean/Betree/Types.lean +++ b/tests/lean/Betree/Types.lean @@ -3,6 +3,9 @@ import Base import Betree.TypesExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace betree diff --git a/tests/lean/Betree/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean index 12fce657..f97517a6 100644 --- a/tests/lean/Betree/TypesExternal_Template.lean +++ b/tests/lean/Betree/TypesExternal_Template.lean @@ -3,6 +3,9 @@ -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean index 23ec66b4..7f347661 100644 --- a/tests/lean/Bitwise.lean +++ b/tests/lean/Bitwise.lean @@ -2,6 +2,9 @@ -- [bitwise] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace bitwise diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index ecb91c16..fff74646 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -2,6 +2,9 @@ -- [constants] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace constants diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 2bbc385d..a557cf73 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -2,6 +2,9 @@ -- [demo] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace demo diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 1b1d5cdf..cd1883e5 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -4,6 +4,9 @@ import Base import External.Types import External.FunsExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace external diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index 870a79c0..51050b21 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -4,6 +4,9 @@ import Base import External.Types open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false open external /- [core::cell::{core::cell::Cell#10}::get]: diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean index 836ddff0..50446e1c 100644 --- a/tests/lean/External/Types.lean +++ b/tests/lean/External/Types.lean @@ -3,6 +3,9 @@ import Base import External.TypesExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace external diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean index 24687d83..2cfbcc80 100644 --- a/tests/lean/External/TypesExternal_Template.lean +++ b/tests/lean/External/TypesExternal_Template.lean @@ -3,6 +3,9 @@ -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false /- [core::cell::Cell] Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/cell.rs', lines 294:0-294:26 diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index f5d028db..7972b715 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -4,6 +4,9 @@ import Base import Hashmap.Types import Hashmap.FunsExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace hashmap diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean index 80362a92..ea5ceed3 100644 --- a/tests/lean/Hashmap/FunsExternal_Template.lean +++ b/tests/lean/Hashmap/FunsExternal_Template.lean @@ -4,6 +4,9 @@ import Base import Hashmap.Types open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false open hashmap /- [hashmap::utils::deserialize]: diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean index 93af883e..6f5d99a5 100644 --- a/tests/lean/Hashmap/Types.lean +++ b/tests/lean/Hashmap/Types.lean @@ -3,6 +3,9 @@ import Base import Hashmap.TypesExternal open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace hashmap diff --git a/tests/lean/Hashmap/TypesExternal_Template.lean b/tests/lean/Hashmap/TypesExternal_Template.lean index 03c3d157..b6f24513 100644 --- a/tests/lean/Hashmap/TypesExternal_Template.lean +++ b/tests/lean/Hashmap/TypesExternal_Template.lean @@ -3,6 +3,9 @@ -- This is a template file: rename it to "TypesExternal.lean" and fill the holes. import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false /- The state type used in the state-error monad -/ axiom State : Type diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean index b8c2343e..b5986ed8 100644 --- a/tests/lean/InfiniteLoop.lean +++ b/tests/lean/InfiniteLoop.lean @@ -2,6 +2,9 @@ -- [infinite_loop] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace infinite_loop diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean index 4eb23934..730d1aa6 100644 --- a/tests/lean/Issue194RecursiveStructProjector.lean +++ b/tests/lean/Issue194RecursiveStructProjector.lean @@ -2,6 +2,9 @@ -- [issue_194_recursive_struct_projector] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace issue_194_recursive_struct_projector diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index a9e5a499..e676336e 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -2,6 +2,9 @@ -- [loops] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace loops diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean index 9233841b..8d592a85 100644 --- a/tests/lean/Matches.lean +++ b/tests/lean/Matches.lean @@ -2,6 +2,9 @@ -- [matches] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace matches diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index f0438050..090ca2b2 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -2,6 +2,9 @@ -- [no_nested_borrows] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace no_nested_borrows diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 03b96903..b1aef703 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -2,6 +2,9 @@ -- [paper] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace paper diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index ed279d58..489871ba 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -2,6 +2,9 @@ -- [polonius_list] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace polonius_list diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 0dd692fe..51aba5bf 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -2,6 +2,9 @@ -- [traits] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace traits diff --git a/tests/lean/misc/MutuallyRecursiveTraits.lean b/tests/lean/misc/MutuallyRecursiveTraits.lean index b0fcb9e9..05871009 100644 --- a/tests/lean/misc/MutuallyRecursiveTraits.lean +++ b/tests/lean/misc/MutuallyRecursiveTraits.lean @@ -2,5 +2,8 @@ -- [mutually_recursive_traits] import Base open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false namespace mutually_recursive_traits diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index e2ed3abc..9b3b0737 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -12,6 +12,6 @@ Uncaught exception: Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 963, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1512, characters 5-42 Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66 -- cgit v1.3.1