gistfile1.txt

;; AVL Tree

(deftype-alias AVLL [A X] (AVL (refine v A (< v X))))
(deftype-alias AVLR [A X] (AVL (refine v A (> v X))))

;; ---- Data declaration (every Node verifies BST + balance + height) ----

(deftype AVL [A]
  (Leaf)
  (Node :key    A
        :left   (AVLL A key)
        :right  (refine v (AVLR A key) (is-bal? left v 1))
        :height (refine v int (is-real? v left right))))

;; ---- Measures (LH equivalents) ----

(defmeasure avl-height :: (forall [A] (-> (AVL A) int))
  (fn [t] (if (Leaf? t) 0 (Node-height t))))

(defmeasure node-height :: (forall [A] (-> (AVL A) (AVL A) int))
  (fn [l r] (+ 1 (max (avl-height l) (avl-height r)))))

(defmeasure is-bal? :: (forall [A] (-> (AVL A) (AVL A) int bool))
  (fn [l r n]
    (<= (abs (- (avl-height l) (avl-height r))) n)))

(defmeasure is-real? :: (forall [A] (-> int (AVL A) (AVL A) bool))
  (fn [v l r] (= v (node-height l r))))

;; ---- Smart constructor + balance helpers ----
;;
;; `node-h` is LH's `node` — fills in the height. `bal-rot-*` are the
;; six classic AVL rotations. `bal` is LH's case-analysis dispatcher.

(define node-h :: (-> int (AVL int) (AVL int) (AVL int))
  (fn [k l r]
    (Node k l r (+ 1 (max (avl-height l) (avl-height r))))))

(define singleton :: (-> int (AVL int))
  (fn [k] (node-h k (Leaf) (Leaf))))

;; Single right rotate (left subtree single-heavy on the left).
(define bal-LL :: (-> int (AVL int) (AVL int) (AVL int))
  (fn [v l r]
    (if (Leaf? l)
        (node-h v l r)
        (node-h (Node-key l)
                (Node-left l)
                (node-h v (Node-right l) r)))))

;; Double rotate left-right.
(define bal-LR :: (-> int (AVL int) (AVL int) (AVL int))
  (fn [v l r]
    (if (Leaf? l)
        (node-h v l r)
        (let [lr (Node-right l)]
          (if (Leaf? lr)
              (node-h v l r)
              (node-h (Node-key lr)
                      (node-h (Node-key l)
                              (Node-left l)
                              (Node-left lr))
                      (node-h v
                              (Node-right lr)
                              r)))))))

;; Single left rotate (mirror of bal-LL).
(define bal-RR :: (-> int (AVL int) (AVL int) (AVL int))
  (fn [v l r]
    (if (Leaf? r)
        (node-h v l r)
        (node-h (Node-key r)
                (node-h v l (Node-left r))
                (Node-right r)))))

;; Double rotate right-left.
(define bal-RL :: (-> int (AVL int) (AVL int) (AVL int))
  (fn [v l r]
    (if (Leaf? r)
        (node-h v l r)
        (let [rl (Node-left r)]
          (if (Leaf? rl)
              (node-h v l r)
              (node-h (Node-key rl)
                      (node-h v l (Node-left rl))
                      (node-h (Node-key r)
                              (Node-right rl)
                              (Node-right r))))))))

;; Dispatcher: pick the rotation based on the imbalance pattern.
(define bal :: (-> int (AVL int) (AVL int) (AVL int))
  (fn [x l r]
    (if (> (- (avl-height l) (avl-height r)) 1)
        ;; left-heavy
        (if (Leaf? l)
            (node-h x l r)
            (if (>= (avl-height (Node-left l))
                    (avl-height (Node-right l)))
                (bal-LL x l r)
                (bal-LR x l r)))
        (if (> (- (avl-height r) (avl-height l)) 1)
            ;; right-heavy
            (if (Leaf? r)
                (node-h x l r)
                (if (>= (avl-height (Node-right r))
                        (avl-height (Node-left r)))
                    (bal-RR x l r)
                    (bal-RL x l r)))
            (node-h x l r)))))

;; Balanced insert: dispatches into bal after recursive insert.
(define insert :: (-> int (AVL int) (AVL int))
  (fn [y t]
    (if (Leaf? t)
        (singleton y)
        (if (= y (Node-key t))
            t
            (if (< y (Node-key t))
                (bal (Node-key t) (insert y (Node-left t)) (Node-right t))
                (bal (Node-key t) (Node-left t) (insert y (Node-right t))))))))

;; ---- Use site ----

(define t0 :: (AVL int) (Leaf))
(define t1 :: (AVL int) (insert 5 t0))
(define t2 :: (AVL int) (insert 3 t1))
(define t3 :: (AVL int) (insert 7 t2))
(define t4 :: (AVL int) (insert 9 t3))
(define t5 :: (AVL int) (insert 1 t4))

;; A skewed sequence that the rotations must rebalance:
;;   1 → 2 → 3 → 4 → 5
;; without rebalancing this would produce a height-5 right-skew chain.
(define skew :: (AVL int)
  (insert 5 (insert 4 (insert 3 (insert 2 (insert 1 (Leaf)))))))

t1
t2
t3
t4
t5
(avl-height t5)
skew
(avl-height skew)