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