#lang scribble/doc
@(require scribble/manual scribble/eval "../evaluator.ss"
(for-label "../../lang/dracula.ss"))
@title[(scheme "avl-rational-keys")]
@specform[(include-book "avl-rational-keys" :dir :teachpacks)]
Documentation under construction.
@verbatim{
;;=============================================================================
;; Function usage notes
;;
;; 1. (avl-retrieve tr key)
;; assumes
;; tr has been constructed by one of the AVL-tree constructors
;; (empty-tree, avl-insert, and avl-delete)
;; new-key is a rational number
;;
;; delivers
;; either a two element list (k d)
;; such that k equals key and
;; tr contains a subtree with k and d in its root
;; or nil, in case key does not occur in tr
;;
;; 2. (empty-tree)
;; delivers an empty AVL-tree
;;
;; 3. (avl-insert tr key datum)
;; assumes
;; tr has been constructed by the AVL-tree constructors
;; (empty-tree, avl-insert, or avl-delete)
;; key is a rational number
;; delivers an AVL tree with the following property
;; (and (equal (avl-retrieve (avl-insert tr key datum) key)
;; (list key datum))
;; (iff (avl-retrieve (avl-insert tr key datum) k)
;; (or (avl-retrieve tr k)
;; (key= k key))))
;;
;; 4. (avl-delete tr key)
;; assumes
;; tr has been constructed by the AVL-tree constructors
;; (empty-tree, avl-insert, and avl-delete)
;; key is a rational number
;; delivers an AVL tree with the following property
;; (equal (avl-retrieve (avl-delete tr key) key)
;; nil)
;;
;; 5. (avl-flatten tr)
;; assumes
;; tr has been constructed by the AVL-tree constructors
;; (empty-tree, avl-insert, and avl-delete)
;; delivers a list of cons-pairs with the following properties
;; (and (implies (occurs-in-tree? k tr)
;; (and (occurs-in-pairs? k (avl-flatten tr))
;; (meta-property-DF tr k)))
;; (implies (not (occurs-in-tree? k tr))
;; (not (occurs-in-pairs? k (avl-flatten tr)))))
;; (increasing-pairs? (avl-flatten tr)))
;; where (meta-property-DF tr k) means that one of the elements, e, in
;; the list (avl-flatten tr) satisfies (equal (car e) k)) and
;; (cadr e) is the datum at the root of the subtree of tr where k occurs
;;
;;=============================================================================
}