Как зациклить, используя рекурсию в ACL2?

Question

Мне нужно сделать что-то подобное, но в ACL2:

for (i=1; i<10; i++) {
    print i;
}

Он использует COMMON LISP, но я понятия не имею, как выполнить эту задачу ...

Мыне может использовать стандартные конструкции Common Lisp, такие как LOOP, DO.Просто рекурсия.

У меня есть несколько ссылок, но мне очень трудно понять:

• Нежное введение в программирование ACL2

Answer 1

В разделе «Посещение всех натуральных чисел от n до 0» в Небольшое введение в программирование ACL2 объясняется, как это сделать.

В вашем случае вы хотите посетить числа вв порядке возрастания, поэтому ваш код должен выглядеть примерно так:

(defun visit (n max ...)
  (cond ((> n max) ...)             ; N exceeds MAX: nothing to do.
        (t .                        ; N less than or equal to MAX:
            . n                     ; do something with N, and
             .
              (visit (+ n 1) max ...) ; visit the numbers above it.
             .
            .
           .)))

Answer 2

(defun foo-loop (n) (cond ((zp n) "сделано") (t (prog2 $ (cw "~ x0" n) (foo-loop (1-n)))))

(foo-loop 10)

Вы можете повторить условие завершения и рекурсию для имитации с 1 по 10

Answer 3

Решение, использующее рекурсию:

> (defun for-loop (from to fn)
    (if (<= from to)
       (progn
         (funcall fn from)
         (for-loop (+ from 1) to fn))))

;; Test
> (for-loop 1 10 #'(lambda (i) (format t "~a~%" i)))
1
2
3
4
5
6
7
8
9
10
NIL