From 661601222ef3787b0b9d84bd7037f42d3ce1f53f Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Thu, 14 Jul 2022 00:44:53 +0900
Subject: huffman-encode: Rearrange codes.

---
 huffman-encode.lisp | 123 +++++++++++++++++++++++++---------------------------
 1 file changed, 58 insertions(+), 65 deletions(-)

(limited to 'huffman-encode.lisp')

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)))
 
-- 
cgit v1.2.3