diff options
Diffstat (limited to 'Notraits.thy')
| -rw-r--r-- | Notraits.thy | 114 |
1 files changed, 114 insertions, 0 deletions
diff --git a/Notraits.thy b/Notraits.thy new file mode 100644 index 0000000..fd459f7 --- /dev/null +++ b/Notraits.thy @@ -0,0 +1,114 @@ +(** 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
\ No newline at end of file |