From 60ec110ebfe85ecbadf2641bdc5315c619766f0e Mon Sep 17 00:00:00 2001 From: stuebinm Date: Sat, 29 Jun 2024 22:05:40 +0200 Subject: some isabelle/hol verification doesn't do much, just proves that the find function won't cause an error. also removes all uses of rust traits, since these are currently broken on the aeneas side. --- src/main.rs | 43 +++++++++++++++++++------------------------ 1 file changed, 19 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/main.rs b/src/main.rs index 1fa0f35..f42ef81 100644 --- a/src/main.rs +++ b/src/main.rs @@ -4,47 +4,44 @@ pub enum Ordering { Greater, } -trait Ord { - fn cmp(&self, other: &Self) -> Ordering; -} // TODO: la structure AVLNode est extrait comme un inductif à un cas // au lieu d'être extrait comme une structure -struct AVLNode<T> { - value: T, - left: AVLTree<T>, - right: AVLTree<T>, +struct AVLNode { + val: u32, + left: AVLTree, + right: AVLTree, } -type AVLTree<T> = Option<Box<AVLNode<T>>>; +type AVLTree = Option<Box<AVLNode>>; -struct AVLTreeSet<T> { - root: AVLTree<T>, +struct AVLTreeSet { + root: AVLTree, } -impl<T: Ord> AVLTreeSet<T> { +impl AVLTreeSet { pub fn new() -> Self { Self { root: None } } - pub fn find(&self, value: T) -> bool { - let mut current_tree = &self.root; + pub fn find(&mut self, value: u32) -> bool { + let mut current_tree = &mut self.root; while let Some(current_node) = current_tree { - match current_node.value.cmp(&value) { - Ordering::Less => current_tree = ¤t_node.right, + match cmp(¤t_node.val, &value) { + Ordering::Less => current_tree = &mut current_node.right, Ordering::Equal => return true, - Ordering::Greater => current_tree = ¤t_node.left, + Ordering::Greater => current_tree = &mut current_node.left, } } false } - pub fn insert(&mut self, value: T) -> bool { + pub fn insert(&mut self, value: u32) -> bool { let mut current_tree = &mut self.root; while let Some(current_node) = current_tree { - match current_node.value.cmp(&value) { + match cmp(¤t_node.val, &value) { Ordering::Less => current_tree = &mut current_node.right, Ordering::Equal => return false, Ordering::Greater => current_tree = &mut current_node.left, @@ -52,7 +49,7 @@ impl<T: Ord> AVLTreeSet<T> { } *current_tree = Some(Box::new(AVLNode { - value, + val: value, left: None, right: None, })); @@ -61,14 +58,12 @@ impl<T: Ord> AVLTreeSet<T> { } } -impl Ord for u32 { - fn cmp(&self, other: &Self) -> Ordering { - if *self < *other { +fn cmp(a: &u32, other: &u32) -> Ordering { + if *a < *other { Ordering::Less - } else if *self == *other { + } else if *a == *other { Ordering::Equal } else { Ordering::Greater } } -} -- cgit v1.2.3