Below is the session log that J Moore showed during his rump session
talk on LOOP.  Not shown is the setup, because the files are not
publicly available.


ACL2 p!>(loop$ for x in '(a b c d)
               as i from 1
               collect (cons x i))
 ((A . 1) (B . 2) (C . 3) (D . 4))
ACL2 p!>(@ loop$::ans)
((A . 1) (B . 2) (C . 3) (D . 4))
ACL2 p!>(loop$ for i from 10 downto 1 by 2
               when (evenp i)
               collect i)
 (10 8 6 4 2)
ACL2 p!>(loop$ for i from 1 to 100
               while (< i 10)
               when (evenp i)
               collect (* i i))
 (4 16 36 64)
ACL2 p!>(loop$ for x in '(a b a c a d b e)
               when (not (member x ans))
               collect x into ans
               finally (return ans))
 (A B C D E)
ACL2 p!>(loop$ for x in (loop$ for i from 1 to 10
                               when (evenp i)
                               collect i)
               append (loop$ for j from 1 to x collect x))
 (2 2 4 4 4 4 6 6 6 6 6 6 8 8 8
    8 8 8 8 8 10 10 10 10 10 10 10 10 10 10)
ACL2 p!>(loop$ for i from -10 to 10
               minimize (* i i))
 0
ACL2 p!>(loop$ for i from -10 to 10
               maximize (* i i))
 100
ACL2 p!>(loop$ for i downto 10 collect i)


ACL2 Error in LOOP$:  [ERROR 6] You must specify an initial value for
I in (LOOP$ FOR I DOWNTO # ...) with a FROM or DOWNFROM clause because
you are stepping downwards and Common Lisp does not specify a default
initial value in this case.

ACL2 p!>(loop$ for i from 1 to 10
               collect i
               finally (return nil))


ACL2 Error in LOOP$:  [ERROR 65] ACL2's LOOP$ statement prohibits FINALLY
unless it is accompanied by an accumulation (e.g., COLLECT) INTO some
variable and this is not the case in 
(LOOP$ FOR I FROM # TO # COLLECT I FINALLY #).

ACL2 p!>(loop$ for v from 0 on '(1 2 3) collect v)


ACL2 Error in LOOP$:  [ERROR 45] You cannot specify two ranges for
V but that is what you seem to be doing in (LOOP$ FOR V FROM # ON # ...).

ACL2 p!>(LOOP$ for v in '(a b c)
               always (symbolp v)
               when (atom v))


ACL2 Error in LOOP$:  [ERROR 16] ACL2's LOOP$ prohibits the combination
of ALWAYS and WHEN clauses as you have written in 
(LOOP$ FOR V IN # ALWAYS # WHEN ...).  (There are cases where Common
Lisp allows something similar but they involve features of LOOP$ not
supported by ACL2.)

ACL2 p!>(loop$ for i from -10 to 10
               when (> i 20)
               maximize (* i i))


HARD ACL2 ERROR in MAXIMIZE:  During the execution of a maximizing
LOOP$ statement the MAXIMIZE expression was never executed, but Common
Lisp requires it to be executed at least once.  This can happen in
several ways, including a maximizing LOOP$ having an empty range, or
having a WHEN or UNLESS clause that excludes all the elements in the
range, or having a WHILE or UNTIL that stops iteration earlier than
expected.



ACL2 Error in ( MAKE-EVENT (ER-PROGN ...)):  Evaluation aborted.  To
debug see :DOC print-gv, see :DOC trace, and see :DOC wet.



ACL2 Error in ( MAKE-EVENT (ER-PROGN ...)):  See :DOC failure.



ACL2 Error in ( ENCAPSULATE NIL (LOGIC) ...):  See :DOC failure.



ACL2 Error in ( MAKE-EVENT (ER-PROGN ...) ...):  Error in MAKE-EVENT
from expansion of:
  (ER-PROGN (ENCAPSULATE NIL (LOGIC)
                         (LOCAL (DEFUN LOOP$::F0 (I LOOP$::ANS)
                                       (DECLARE #)
                                       (IF # # LOOP$::ANS)))
                         (MAKE-EVENT (ER-PROGN (ASSIGN LOOP$::ANS #)
                                               (VALUE #))))
            (VALUE '(VALUE-TRIPLE NIL)))
(See :DOC set-iprint to be able to see elided values in this message.)



ACL2 Error in ( MAKE-EVENT (ER-PROGN ...) ...):  See :DOC failure.

ACL2 p!>(time$ (LOOP$ for i from 1 to 10000000
                      always (integerp i)))
; (EV-REC *RETURN-LAST-ARG3* ...) took 
; 0.07 seconds realtime, 0.07 seconds runtime
; (237,824 bytes allocated).
 T
ACL2 p!>(value :q)

Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
? (time (LOOP for i from 1 to 10000000
              always (integerp i)))
(LOOP FOR I FROM 1 TO 10000000 ALWAYS (INTEGERP I))
took 25,675 microseconds (0.025675 seconds) to run.
During that period, and with 8 available CPU cores,
     25,627 microseconds (0.025627 seconds) were spent in user mode
         57 microseconds (0.000057 seconds) were spent in system mode
T
? (lp)

ACL2 Version 7.1.  Level 1.  Cbd "/Users/moore/".
System books directory "/Users/moore/work/git-acl2-26-05-15/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 p!>(trn (append xxx
                     (loop$ for x in aaa
                            when (evenp x)
                            collect (cons x yyy))))
(1 ((DEFUN LOOP$::F0 (X-LST LOOP$::ANS YYY)
           (DECLARE (XARGS :MODE :PROGRAM
                           :MEASURE (ACL2-COUNT X-LST)))
           (IF (ENDP X-LST)
               (REVAPPEND LOOP$::ANS NIL)
               (LET ((X (CAR X-LST)))
                    (DECLARE (IGNORABLE X))
                    (LOOP$::F0 (CDR X-LST)
                               (IF (CHECK-VARS-NOT-FREE (LOOP$::ANS)
                                                        (EVENP X))
                                   (CONS (CHECK-VARS-NOT-FREE (LOOP$::ANS)
                                                              (CONS X YYY))
                                         LOOP$::ANS)
                                   LOOP$::ANS)
                               YYY)))))
   (APPEND XXX (LOOP$::F0 AAA NIL YYY)))
ACL2 p!>(trn (loop$ for x in (loop$ for i from 1 to 10
				    when (evenp i)
				    collect i)
		    append (loop$ for j from 1 to x
                                  collect x)))
(3
 ((DEFUN
   LOOP$::F0 (X-LST LOOP$::ANS)
   (DECLARE (XARGS :MODE :PROGRAM
                   :MEASURE (ACL2-COUNT X-LST)))
   (IF (ENDP X-LST)
       (REVAPPEND LOOP$::ANS NIL)
       (LET ((X (CAR X-LST)))
            (DECLARE (IGNORABLE X))
            (LOOP$::F0 (CDR X-LST)
                       (REVAPPEND (CHECK-VARS-NOT-FREE (LOOP$::ANS)
                                                       (LOOP$::F2 1 X NIL X))
                                  LOOP$::ANS)))))
  (DEFUN LOOP$::F2 (J J-BOUND LOOP$::ANS X)
         (DECLARE (XARGS :MODE :PROGRAM
                         :MEASURE (UP->-MEASURE J J-BOUND 1)))
         (IF (AND (RATIONALP J) (RATIONALP J-BOUND))
             (IF (> J J-BOUND)
                 (REVAPPEND LOOP$::ANS NIL)
                 (LOOP$::F2 (+ J 1)
                            J-BOUND (CONS X LOOP$::ANS)
                            X))
             LOOP$::ANS))
  (DEFUN LOOP$::F1 (I LOOP$::ANS)
         (DECLARE (XARGS :MODE :PROGRAM
                         :MEASURE (UP->-MEASURE I 10 1)))
         (IF (RATIONALP I)
             (IF (> I 10)
                 (REVAPPEND LOOP$::ANS NIL)
                 (LOOP$::F1 (+ I 1)
                            (IF (CHECK-VARS-NOT-FREE (LOOP$::ANS)
                                                     (EVENP I))
                                (CONS I LOOP$::ANS)
                                LOOP$::ANS)))
             LOOP$::ANS)))
 (LOOP$::F0 (LOOP$::F1 1 NIL) NIL))
ACL2 p!>(loop$ named count-by-sevenths
               for i from 0 to 5 by 1/7
               collect i)
 (0 1/7 2/7 3/7 4/7 5/7 6/7 1 8/7 9/7 10/7
    11/7 12/7 13/7 2 15/7 16/7 17/7 18/7
    19/7 20/7 3 22/7 23/7 24/7 25/7 26/7
    27/7 4 29/7 30/7 31/7 32/7 33/7 34/7 5)
ACL2 p!>(trn (loop$ named count-by-sevenths
                    for i from 0 to 5 by 1/7
                    collect i))
(1 ((DEFUN COUNT-BY-SEVENTHS (I LOOP$::ANS)
           (DECLARE (XARGS :MODE :PROGRAM
                           :MEASURE (UP->-MEASURE I 5 1/7)))
           (IF (RATIONALP I)
               (IF (> I 5)
                   (REVAPPEND LOOP$::ANS NIL)
                   (COUNT-BY-SEVENTHS (+ I 1/7)
                                      (CONS I LOOP$::ANS)))
               LOOP$::ANS)))
   (COUNT-BY-SEVENTHS 0 NIL))
ACL2 p!>(DEFUN COUNT-BY-SEVENTHS (I LOOP$::ANS)
           (DECLARE (XARGS :MODE :PROGRAM
                           :MEASURE (UP->-MEASURE I 5 1/7)))
           (IF (RATIONALP I)
               (IF (> I 5)
                   (REVAPPEND LOOP$::ANS NIL)
                   (COUNT-BY-SEVENTHS (+ I 1/7)
                                      (CONS I LOOP$::ANS)))
               LOOP$::ANS))

Summary
Form:  ( DEFUN COUNT-BY-SEVENTHS ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 COUNT-BY-SEVENTHS
ACL2 p!>(logic)
ACL2 !>(verify-termination count-by-sevenths)

For the admission of COUNT-BY-SEVENTHS we will use the relation O<
(which is known to be well-founded on the domain recognized by O-P)
and the measure (UP->-MEASURE I 5 1/7).  The non-trivial part of the
measure conjecture is

Goal
(AND (O-P (UP->-MEASURE I 5 1/7))
     (IMPLIES (AND (RATIONALP I) (<= I 5))
              (O< (UP->-MEASURE (+ I 1/7) 5 1/7)
                  (UP->-MEASURE I 5 1/7)))).
Subgoal 2
Subgoal 1
Subgoal 1'

Q.E.D.

That completes the proof of the measure theorem for COUNT-BY-SEVENTHS.
Thus, we admit this function under the principle of definition.  We
observe that the type of COUNT-BY-SEVENTHS is described by the theorem
(OR (OR (CONSP (COUNT-BY-SEVENTHS I LOOP$::ANS))
        (EQUAL (COUNT-BY-SEVENTHS I LOOP$::ANS)
               NIL))
    (EQUAL (COUNT-BY-SEVENTHS I LOOP$::ANS)
           LOOP$::ANS)).
We used the :executable-counterpart of TRUE-LISTP, primitive type reasoning
and the :type-prescription rule TRUE-LISTP-REVAPPEND-TYPE-PRESCRIPTION.

Summary
Form:  ( DEFUN COUNT-BY-SEVENTHS ...)
Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART TRUE-LISTP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR UP->-MEASURE-WORKS . 2)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:TYPE-PRESCRIPTION TRUE-LISTP-REVAPPEND-TYPE-PRESCRIPTION)
        (:TYPE-PRESCRIPTION UP->-MEASURE-WORKS))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  150

Summary
Form:  ( MAKE-EVENT (VERIFY-TERMINATION-FN ...))
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  150
 COUNT-BY-SEVENTHS
ACL2 !>(trn (loop$ for x in '(a b a c a d b e)
		    when (not (member x ans))
		    collect x into ans
		    finally (return ans)))
(1 ((DEFUN LOOP$::F0 (X-LST ANS)
           (DECLARE (XARGS :MODE :PROGRAM
                           :MEASURE (ACL2-COUNT X-LST)))
           (IF (ENDP X-LST)
               (LET ((ANS (REVAPPEND ANS NIL))) ANS)
               (LET ((X (CAR X-LST)))
                    (DECLARE (IGNORABLE X))
                    (LOOP$::F0 (CDR X-LST)
                               (IF (LET ((ANS (REVAPPEND ANS NIL)))
                                        (NOT (MEMBER X ANS)))
                                   (CONS X ANS)
                                   ANS))))))
   (LOOP$::F0 '(A B A C A D B E) NIL))
ACL2 !>(quote issues)
ISSUES
ACL2 !>(quote (:logic v :exec -- :exec should be CLTL and :logic can be simpler than here))
(:LOGIC V :EXEC -- :EXEC SHOULD BE CLTL
        AND :LOGIC CAN BE SIMPLER THAN HERE)
ACL2 !>(quote (but we must support proofs about LOOP))
(BUT WE MUST SUPPORT PROOFS ABOUT LOOP)
ACL2 !>(quote (idea -- :logic should be compositions of maps and filters with automatic support for fn instantiation))
(IDEA -- :LOGIC SHOULD
      BE COMPOSITIONS OF MAPS AND FILTERS WITH
      AUTOMATIC SUPPORT FOR FN INSTANTIATION)
ACL2 !>Bye.