-- 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