From 22e1d6c1abc5c7c825364658deab9969190586a6 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 13 Aug 2021 23:22:19 +0900
Subject: permutations: Add guards.

---
 permutations.lisp | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'permutations.lisp')

diff --git a/permutations.lisp b/permutations.lisp
index 4aa9640..d75a4d2 100644
--- a/permutations.lisp
+++ b/permutations.lisp
@@ -1,10 +1,12 @@
 (defun mapcar-cons (e x)
+  (declare (xargs :guard (true-listp x)))
   (if (endp x)
       nil
       (cons (cons e (car x))
             (mapcar-cons e (cdr x)))))
 
 (defun insert (e x)
+  (declare (xargs :guard (true-listp x)))
   (if (endp x)
       (list (list e))
       (cons (cons e x)
@@ -12,47 +14,56 @@
                          (insert e (cdr x))))))
 
 (defun mappend-insert (x y)
+  (declare (xargs :guard (true-list-listp y)))
   (if (endp y)
       nil
       (append (insert x (car y))
               (mappend-insert x (cdr y)))))
 
 (defun permutations (x)
+  (declare (xargs :guard (true-listp x)))
   (if (endp x)
       (list nil)
       (mappend-insert (car x)
                       (permutations (cdr x)))))
 
 (defun factorial (n)
+  (declare (xargs :guard (natp n)))
   (if (zp n)
       1
       (* n (factorial (1- n)))))
 
 (defun mapcar-len (x)
+  (declare (xargs :guard (true-list-listp x)))
   (if (endp x)
       nil
       (cons (len (car x))
             (mapcar-len (cdr x)))))
 
 (defun sum (x)
+  (declare (xargs :guard (nat-listp x)))
   (if (endp x)
       0
       (+ (car x)
          (sum (cdr x)))))
 
 (defun mapcar-sum (x y)
+  (declare (xargs :guard (and (nat-listp x)
+                              (nat-listp y))))
   (if (or (endp x) (endp y))
       nil
       (cons (+ (car x) (car y))
             (mapcar-sum (cdr x) (cdr y)))))
 
 (defun repeat (x n)
+  (declare (xargs :guard (natp n)))
   (if (zp n)
       nil
       (cons x
             (repeat x (1- n)))))
 
 (defun repeatedp (x)
+  (declare (xargs :guard (true-listp x)))
   (if (or (endp x)
           (endp (cdr x)))
       t
-- 
cgit v1.2.3