-- 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 13:0-13:17 -/
inductive AVLNode (T : Type) :=
| mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T

/- [avl_verification::AVLTreeSet]
   Source: 'src/main.rs', lines 21:0-21:20 -/
structure AVLTreeSet (T : Type) where
  root : Option (AVLNode T)

/- [avl_verification::{avl_verification::AVLTreeSet<T>}::new]:
   Source: 'src/main.rs', lines 26:4-26:24 -/
def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) :=
  Result.ok { root := none }

/- [avl_verification::{avl_verification::AVLTreeSet<T>}::find]: loop 0:
   Source: 'src/main.rs', lines 30:4-42:5 -/
divergent def AVLTreeSet.find_loop
  (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (AVLNode T))
  :
  Result Bool
  :=
  match current_tree with
  | none => Result.ok false
  | some current_node =>
    do
    let ⟨ t, current_tree1, current_tree2 ⟩ := current_node
    let o ← OrdInst.cmp t value
    match o with
    | Ordering.Less => AVLTreeSet.find_loop T OrdInst value current_tree2
    | Ordering.Equal => Result.ok true
    | Ordering.Greater => AVLTreeSet.find_loop T OrdInst value current_tree1

/- [avl_verification::{avl_verification::AVLTreeSet<T>}::find]:
   Source: 'src/main.rs', lines 30:4-30:40 -/
def AVLTreeSet.find
  (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) :
  Result Bool
  :=
  AVLTreeSet.find_loop T OrdInst value self.root

/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0:
   Source: 'src/main.rs', lines 43:4-61: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.ok (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, current_tree3) ←
        AVLTreeSet.insert_loop T OrdInst value current_tree2
      Result.ok (b, some (AVLNode.mk t current_tree1 current_tree3))
    | Ordering.Equal =>
      Result.ok (false, some (AVLNode.mk t current_tree1 current_tree2))
    | Ordering.Greater =>
      do
      let (b, current_tree3) ←
        AVLTreeSet.insert_loop T OrdInst value current_tree1
      Result.ok (b, some (AVLNode.mk t current_tree3 current_tree2))

/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]:
   Source: 'src/main.rs', lines 43:4-43:46 -/
def AVLTreeSet.insert
  (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) :
  Result (Bool × (AVLTreeSet T))
  :=
  do
  let (b, u) ← AVLTreeSet.insert_loop T OrdInst value self.root
  Result.ok (b, { root := u })

/- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]:
   Source: 'src/main.rs', lines 65:4-65:43 -/
def OrdU32.cmp (self : U32) (other : U32) : Result Ordering :=
  if self < other
  then Result.ok Ordering.Less
  else
    if self = other
    then Result.ok Ordering.Equal
    else Result.ok Ordering.Greater

/- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}]
   Source: 'src/main.rs', lines 64:0-64:16 -/
def OrdU32 : Ord U32 := {
  cmp := OrdU32.cmp
}

end avl_verification