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 = &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
         }
     }
-}
-- 
cgit v1.2.3