Initial extraction

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>

1 files changed, 87 insertions, 0 deletions

diff --git a/AvlVerification.lean b/AvlVerification.lean
new file mode 100644
index 0000000..e0516b4
--- /dev/null
+++ b/AvlVerification.lean
@@ -0,0 +1,87 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [avl_verification]
+import Base
+open Primitives
+
+namespace avl_verification
+
+/- [avl_verification::Ordering]
+   Source: 'src/main.rs', lines 1:0-1:17 -/
+inductive Ordering :=
+| Less : Ordering
+| Equal : Ordering
+| Greater : Ordering
+
+/- Trait declaration: [avl_verification::Ord]
+   Source: 'src/main.rs', lines 7:0-7:9 -/
+structure Ord (Self : Type) where
+  cmp : Self → Self → Result Ordering
+
+/- [avl_verification::AVLNode]
+   Source: 'src/main.rs', lines 11:0-11:17 -/
+inductive AVLNode (T : Type) :=
+| mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T
+
+/- [avl_verification::AVLTreeSet]
+   Source: 'src/main.rs', lines 19:0-19:20 -/
+structure AVLTreeSet (T : Type) where
+  root : Option (AVLNode T)
+
+/- [avl_verification::{avl_verification::AVLTreeSet<T>}::new]:
+   Source: 'src/main.rs', lines 24:4-24:24 -/
+def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) :=
+  Result.ret { root := none }
+
+/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0:
+   Source: 'src/main.rs', lines 28:4-46:5 -/
+divergent def AVLTreeSet.insert_loop
+  (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (AVLNode T))
+  :
+  Result (Bool × (Option (AVLNode T)))
+  :=
+  match current_tree with
+  | none => let a := AVLNode.mk value none none
+            Result.ret (true, some a)
+  | some current_node =>
+    do
+    let ⟨ t, current_tree1, current_tree2 ⟩ := current_node
+    let o ← OrdInst.cmp t value
+    match o with
+    | Ordering.Less =>
+      do
+      let (b, back) ← AVLTreeSet.insert_loop T OrdInst value current_tree2
+      Result.ret (b, some (AVLNode.mk t current_tree1 back))
+    | Ordering.Equal =>
+      Result.ret (false, some (AVLNode.mk t current_tree1 current_tree2))
+    | Ordering.Greater =>
+      do
+      let (b, back) ← AVLTreeSet.insert_loop T OrdInst value current_tree1
+      Result.ret (b, some (AVLNode.mk t back current_tree2))
+
+/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]:
+   Source: 'src/main.rs', lines 28:4-28:46 -/
+def AVLTreeSet.insert
+  (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) :
+  Result (Bool × (AVLTreeSet T))
+  :=
+  do
+  let (b, back) ← AVLTreeSet.insert_loop T OrdInst value self.root
+  Result.ret (b, { root := back })
+
+/- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]:
+   Source: 'src/main.rs', lines 50:4-50:43 -/
+def OrdU32.cmp (self : U32) (other : U32) : Result Ordering :=
+  if self < other
+  then Result.ret Ordering.Less
+  else
+    if self = other
+    then Result.ret Ordering.Equal
+    else Result.ret Ordering.Greater
+
+/- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}]
+   Source: 'src/main.rs', lines 49:0-49:16 -/
+def OrdU32 : Ord U32 := {
+  cmp := OrdU32.cmp
+}
+
+end avl_verification