huffman-encode: Rearrange functions and thiorems.

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))))