summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--huffman-encode.lisp123
1 files changed, 58 insertions, 65 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp
index 17c9c72..edc05f1 100644
--- a/huffman-encode.lisp
+++ b/huffman-encode.lisp
@@ -284,70 +284,6 @@
(cons (list (car x) c)
(message-to-pairs rest)))))
-
-;;; Huffman encode/decode.
-(defun encode-1 (x tree)
- (declare (xargs :guard (huffman-treep tree)
- :measure (node-count tree)))
- (if (nodep tree)
- (cond ((member-equal x (symbol-list (left tree)))
- (cons 0 (encode-1 x (left tree))))
- (t
- (cons 1 (encode-1 x (right tree)))))
- nil))
-
-(defun encode (x tree)
- (declare (xargs :guard (and (true-listp x)
- (nodep tree)
- (huffman-treep tree))))
- (if (endp x)
- nil
- (append (encode-1 (car x) tree)
- (encode (cdr x) tree))))
-
-
-(defun bit-listp (x)
- (declare (xargs :guard t))
- (if (atom x)
- (null x)
- (and (bitp (car x))
- (bit-listp (cdr x)))))
-
-(defun decode-1 (x tree)
- (declare (xargs :guard (and (bit-listp x)
- (huffman-treep tree))
- :measure (node-count tree)))
- (cond ((and (consp x) (nodep tree))
- (if (equal (car x) 0)
- (decode-1 (cdr x) (left tree))
- (decode-1 (cdr x) (right tree))))
- ((nodep tree) (mv nil nil))
- (t
- (mv (leaf-symbol tree) x))))
-
-(defun decode (x tree)
- (declare (xargs :measure (len x)
- :guard (and (bit-listp x)
- (nodep tree)
- (huffman-treep tree))))
- (if (or (endp x)
- (not (nodep tree)))
- nil
- (mv-let (symbol rest)
- (decode-1 x tree)
- (cons symbol (decode rest tree)))))
-
-
-;;; --- defthm: pairs ---
-
-(defthm rationalp-0-count-and-remove
- (rationalp (car (count-and-remove e x))))
-
-(defthm symbol-weight-pair-listp-message-to-pairs
- (symbol-weight-pair-listp (message-to-pairs x)))
-
-;; --- insert - generate
-
(defthm huffman-tree-listp-insert
(implies (and (huffman-tree-listp x)
(huffman-treep e))
@@ -401,7 +337,64 @@
(< 1 (len x)))
(huffman-treep (generate-huffman-tree x))))
-;;; ----- decode-encode
+(defthm rationalp-0-count-and-remove
+ (rationalp (car (count-and-remove e x))))
+
+(defthm symbol-weight-pair-listp-message-to-pairs
+ (symbol-weight-pair-listp (message-to-pairs x)))
+
+;;; Huffman encodeing and decoding.
+(defun encode-1 (x tree)
+ (declare (xargs :guard (huffman-treep tree)
+ :measure (node-count tree)))
+ (if (nodep tree)
+ (cond ((member-equal x (symbol-list (left tree)))
+ (cons 0 (encode-1 x (left tree))))
+ (t
+ (cons 1 (encode-1 x (right tree)))))
+ nil))
+
+(defun encode (x tree)
+ (declare (xargs :guard (and (true-listp x)
+ (nodep tree)
+ (huffman-treep tree))))
+ (if (endp x)
+ nil
+ (append (encode-1 (car x) tree)
+ (encode (cdr x) tree))))
+
+
+(defun bit-listp (x)
+ (declare (xargs :guard t))
+ (if (atom x)
+ (null x)
+ (and (bitp (car x))
+ (bit-listp (cdr x)))))
+
+(defun decode-1 (x tree)
+ (declare (xargs :guard (and (bit-listp x)
+ (huffman-treep tree))
+ :measure (node-count tree)))
+ (cond ((and (consp x) (nodep tree))
+ (if (equal (car x) 0)
+ (decode-1 (cdr x) (left tree))
+ (decode-1 (cdr x) (right tree))))
+ ((nodep tree) (mv nil nil))
+ (t
+ (mv (leaf-symbol tree) x))))
+
+(defun decode (x tree)
+ (declare (xargs :measure (len x)
+ :guard (and (bit-listp x)
+ (nodep tree)
+ (huffman-treep tree))))
+ (if (or (endp x)
+ (not (nodep tree)))
+ nil
+ (mv-let (symbol rest)
+ (decode-1 x tree)
+ (cons symbol (decode rest tree)))))
+
(defthm bit-listp-encode-1
(bit-listp (encode-1 x tree)))