(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [avl_verification] *)
theory "Notraits" imports
  "Aeneas.Primitives"
  "HOL-Library.Datatype_Records"
begin


(*[avl_verification::Ordering]
   Source: 'src/main.rs', lines 1:0-1:17*)
datatype Ordering = Ordering_Less | Ordering_Equal | Ordering_Greater


(*[avl_verification::AVLNode]
   Source: 'src/main.rs', lines 10:0-10:14*)
datatype AVLNode = mkAVLNode
  (val: "u32") (left: "AVLNode option") (right: "AVLNode option")
local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>AVLNode\<close>\<close>

(*[avl_verification::AVLTreeSet]
   Source: 'src/main.rs', lines 18:0-18:17*)
datatype AVLTreeSet = mkAVLTreeSet (root: "AVLNode option")
local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>AVLTreeSet\<close>\<close>

(*[avl_verification::{avl_verification::AVLTreeSet}::new]:
   Source: 'src/main.rs', lines 23:4-23:24*)
definition aVLTreeSet_new :: "AVLTreeSet result" where
  "aVLTreeSet_new = Ok (\<lparr> root = None \<rparr>)"

(*[avl_verification::cmp]:
   Source: 'src/main.rs', lines 61:0-61:40*)
fun cmp :: "u32 \<Rightarrow> u32 \<Rightarrow> Ordering result" where
  "cmp a other =
    (if u32_lt a other
    then Ok Ordering_Less
    else (if a = other then Ok Ordering_Equal else Ok Ordering_Greater))"

(*[avl_verification::{avl_verification::AVLTreeSet}::find]: loop 0:
   Source: 'src/main.rs', lines 27:4-39:5*)
function aVLTreeSet_find_loop
  :: "u32 \<Rightarrow> AVLNode option \<Rightarrow> (bool * AVLNode option) result" where
  "aVLTreeSet_find_loop value1 current_tree =
    (case current_tree of
      None \<Rightarrow> Ok (False, None)
    | Some current_node \<Rightarrow>
      do {
        o1 \<leftarrow> cmp (val current_node) value1;
        (case o1 of
          Ordering_Less \<Rightarrow>
          do {
            (b, current_tree1) \<leftarrow>
              aVLTreeSet_find_loop value1 (right current_node);
            Ok (b, Some
              (current_node \<lparr> right := current_tree1 \<rparr>))
            }
        | Ordering_Equal \<Rightarrow> Ok (True, Some current_node)
        | Ordering_Greater \<Rightarrow>
          do {
            (b, current_tree1) \<leftarrow>
              aVLTreeSet_find_loop value1 (left current_node);
            Ok (b, Some (current_node \<lparr> left := current_tree1 \<rparr>))
            })
        })"  by auto

(*[avl_verification::{avl_verification::AVLTreeSet}::find]:
   Source: 'src/main.rs', lines 27:4-27:46*)
fun aVLTreeSet_find
  :: "AVLTreeSet \<Rightarrow> u32 \<Rightarrow> (bool * AVLTreeSet) result" where
  "aVLTreeSet_find self value1 =
    do {
      (b, as) \<leftarrow> aVLTreeSet_find_loop value1 (root self);
      Ok (b, (\<lparr> root = as \<rparr>))
      }"

(*[avl_verification::{avl_verification::AVLTreeSet}::insert]: loop 0:
   Source: 'src/main.rs', lines 40:4-58:5*)
function aVLTreeSet_insert_loop
  :: "u32 \<Rightarrow> AVLNode option \<Rightarrow> (bool * AVLNode option) result" where
  "aVLTreeSet_insert_loop value1 current_tree =
    (case current_tree of
      None \<Rightarrow>
      let a = (\<lparr> val = value1, left = None, right = None \<rparr>) in
        Ok (True, Some a)
    | Some current_node \<Rightarrow>
      do {
        o1 \<leftarrow> cmp (val current_node) value1;
        (case o1 of
          Ordering_Less \<Rightarrow>
          do {
            (b, current_tree1) \<leftarrow>
              aVLTreeSet_insert_loop value1 (right current_node);
            Ok (b, Some
              (current_node \<lparr> right := current_tree1 \<rparr>))
            }
        | Ordering_Equal \<Rightarrow> Ok (False, Some current_node)
        | Ordering_Greater \<Rightarrow>
          do {
            (b, current_tree1) \<leftarrow>
              aVLTreeSet_insert_loop value1 (left current_node);
            Ok (b, Some (current_node \<lparr> left := current_tree1 \<rparr>))
            })
        })"  by auto

(*[avl_verification::{avl_verification::AVLTreeSet}::insert]:
   Source: 'src/main.rs', lines 40:4-40:48*)
fun aVLTreeSet_insert
  :: "AVLTreeSet \<Rightarrow> u32 \<Rightarrow> (bool * AVLTreeSet) result" where
  "aVLTreeSet_insert self value1 =
    do {
      (b, as) \<leftarrow> aVLTreeSet_insert_loop value1 (root self);
      Ok (b, (\<lparr> root = as \<rparr>))
      }"

end