1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
-- 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, as) ← AVLTreeSet.insert_loop T OrdInst value self.root
Result.ok (b, { root := as })
/- [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
|
