diff options
| -rw-r--r-- | huffman-encode.lisp | 123 |
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))) |