some isabelle/hol verificationHEADmain

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.

1 files changed, 19 insertions, 24 deletions

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 = &current_node.right,
+            match cmp(&current_node.val, &value) {
+                Ordering::Less => current_tree = &mut current_node.right,
                 Ordering::Equal => return true,
-                Ordering::Greater => current_tree = &current_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(&current_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
         }
     }
-}