summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--huffman-encode.lisp83
1 files changed, 41 insertions, 42 deletions
diff --git a/huffman-encode.lisp b/huffman-encode.lisp
index be416b3..6da268f 100644
--- a/huffman-encode.lisp
+++ b/huffman-encode.lisp
@@ -180,6 +180,16 @@
node-count))
;;; Generate huffman trees
+(defun symbol-weight-pair-listp (x)
+ (declare (xargs :guard t))
+ (if (atom x)
+ (null x)
+ (and (consp (car x))
+ (consp (cdar x))
+ (rationalp (cadar x))
+ (null (cddar x))
+ (symbol-weight-pair-listp (cdr x)))))
+
(defun huffman-tree-listp (x)
(declare (xargs :guard t))
(if (atom x)
@@ -194,17 +204,6 @@
(orderdp (cdr x)))
(t nil)))
-(defun symbol-weight-pair-listp (x)
- (declare (xargs :guard t))
- (if (atom x)
- (null x)
- (and (consp (car x))
- (consp (cdar x))
- (rationalp (cadar x))
- (null (cddar x))
- (symbol-weight-pair-listp (cdr x)))))
-
-
(defun insert (e x)
(declare (xargs :guard (and (huffman-treep e)
(huffman-tree-listp x))))
@@ -215,6 +214,13 @@
(cons (car x)
(insert e (cdr x))))))
+(defun pairs-to-leaves (x)
+ (declare (xargs :guard (symbol-weight-pair-listp x)))
+ (if (endp x)
+ nil
+ (insert (huffman-leaf (caar x) (cadar x))
+ (pairs-to-leaves (cdr x)))))
+
(defun generate (x a)
(declare (xargs :measure (len x)
:guard (and (huffman-tree-listp x)
@@ -232,13 +238,6 @@
(generate (insert a (cddr x))
(huffman-node (car x) (cadr x))))))
-(defun pairs-to-leaves (x)
- (declare (xargs :guard (symbol-weight-pair-listp x)))
- (if (endp x)
- nil
- (insert (huffman-leaf (caar x) (cadar x))
- (pairs-to-leaves (cdr x)))))
-
(defun generate-huffman-tree (x)
(declare (xargs :guard (and (symbol-weight-pair-listp x)
(< 1 (len x)))
@@ -246,28 +245,6 @@
(let ((leaves (pairs-to-leaves x)))
(generate (cdr leaves) (car leaves))))
-(defun count-and-remove (e x)
- (declare (xargs :guard (true-listp x)))
- (cond ((endp x) (mv 0 nil))
- ((equal e (car x))
- (mv-let (c rest)
- (count-and-remove e (cdr x))
- (mv (+ 1 c) rest)))
- (t
- (mv-let (c rest)
- (count-and-remove e (cdr x))
- (mv c (cons (car x) rest))))))
-
-
-(defun message-to-pairs (x)
- (declare (xargs :guard (true-listp x)))
- (if (endp x)
- nil
- (mv-let (c rest)
- (count-and-remove (car x) x)
- (cons (list (car x) c)
- (message-to-pairs rest)))))
-
(defthm huffman-tree-listp-insert
(implies (and (huffman-tree-listp x)
(huffman-treep e))
@@ -300,8 +277,6 @@
(implies (huffman-tree-listp x)
(huffman-tree-listp (cdr x))))
-(verify-guards generate-huffman-tree)
-
(defthm huffman-treep-car
(implies (and (consp x) (huffman-tree-listp x))
(huffman-treep (car x))))
@@ -321,6 +296,30 @@
(< 1 (len x)))
(huffman-treep (generate-huffman-tree x))))
+(verify-guards generate-huffman-tree)
+
+(defun count-and-remove (e x)
+ (declare (xargs :guard (true-listp x)))
+ (cond ((endp x) (mv 0 nil))
+ ((equal e (car x))
+ (mv-let (c rest)
+ (count-and-remove e (cdr x))
+ (mv (+ 1 c) rest)))
+ (t
+ (mv-let (c rest)
+ (count-and-remove e (cdr x))
+ (mv c (cons (car x) rest))))))
+
+
+(defun message-to-pairs (x)
+ (declare (xargs :guard (true-listp x)))
+ (if (endp x)
+ nil
+ (mv-let (c rest)
+ (count-and-remove (car x) x)
+ (cons (list (car x) c)
+ (message-to-pairs rest)))))
+
(defthm rationalp-0-count-and-remove
(rationalp (car (count-and-remove e x))))