• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Defmacro
        • Loop$-primer
          • Lp-section-8
          • Lp-section-10
          • Lp-section-6
          • Lp-section-9
          • Lp-section-17
          • Lp-section-16
          • Lp-section-15
          • Lp-section-11
          • Lp-section-4
            • Lp-section-7
            • Lp-section-13
            • Lp-section-12
            • Lp-section-14
            • Lp-section-5
            • Lp-section-0
            • Lp-section-2
            • Lp-section-18
            • Lp-section-3
            • Lp-section-1
          • Fast-alists
          • Defconst
          • Evaluation
          • Guard
          • Equality-variants
          • Compilation
          • Hons
          • ACL2-built-ins
          • Developers-guide
          • System-attachments
          • Advanced-features
          • Set-check-invariant-risk
          • Numbers
          • Efficiency
          • Irrelevant-formals
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Redefining-programs
          • Lists
          • Invariant-risk
          • Errors
          • Defabbrev
          • Conses
          • Alists
          • Set-register-invariant-risk
          • Strings
          • Program-wrapper
          • Get-internal-time
          • Basics
          • Packages
          • Oracle-eval
          • Defmacro-untouchable
          • <<
          • Primitive
          • Revert-world
          • Unmemoize
          • Set-duplicate-keys-action
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Fake-oracle-eval
          • Defopen
          • Sleep
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Loop$-primer

    Lp-section-4

    Syntax of FOR Loop$s

    LP4: Syntax of FOR Loop$s

    To describe the syntax of FOR loop$s we first describe the most elaborate FOR loop$. Then we note which elements can be omitted. The most elaborate FOR loop$ is of the form

            (LOOP$ FOR v1 OF-TYPE spec1 target1
                            AS   v2 OF-TYPE spec2 target2
                            ...
                            AS   vn OF-TYPE specn targetn
                            UNTIL :GUARD guard1 until-expr
                            WHEN   :GUARD guard2 when-expr
                            op :GUARD guard3 body-expr)

    where

    • each vi   is a legal variable symbol, they are all distinct, and are collectively called the iteration variables,
    • each speci   is a type-spec for the corresponding variable vi,
    • each targeti is of one of the forms below and specifies the range of values to be taken by the corresponding variable vi. Abstractly you may think of the “range” here simply as a list of the values as described below, where list-expr is a term (which is expected to evaluate to a true list), lo-expr and hi-expr are terms (which are expected to evaluate to integers), and step-expr is a term (which is expected to evaluate to a positive integer). In the examples given below, let rv be the list reverse function, so (rv '(a b c)) is (C B A).
      • IN list-expr — range is the value of list-expr. For example, the range of “IN (rv '(a b c))” is (C B A).
      • ON list-expr — range is the list of successive non-nil tails of the value of list-expr. For example, the range of “ON (rv '(a b c))” is ((C B A) (B A) (A)). The range value is produced by (TAILS list-expr).
      • FROM lo-expr TO hi-expr BY step-expr — If “BY step-expr” is omitted, “BY 1” is used. The range contains all the integers from the value of lo-expr to the greatest integer less than or equal to the value of hi-expr such that each is separated from its higher neighbor by the value of step-expr. For example, the range of “FROM 1 TO 10 BY 2” is (1 3 5 7 9). The range value is produced by (FROM-TO-BY lo-expr hi-expr step-expr).
    • each guardi is a term,
    • each until-expr, when-expr, and body-expr   is a tame term, and
    • op   is one of the operators   SUM, COLLECT, APPEND, ALWAYS, or THEREIS.

    The symbols FOR, IN, ON, FROM, TO, BY, OF-TYPE, WHEN, UNTIL, SUM, COLLECT, APPEND, ALWAYS, and THEREIS when used in loop$ statements may be in any package.

    Common Lisp prohibits loops with both a WHEN clause and either an ALWAYS or a THEREIS operator. For example, if you are tempted to write “WHEN p ALWAYS q” you can instead write “ALWAYS (if p q t).”

    The following elements may be omitted from the most elaborate form and still produce legal loop$ statements:

    • any line beginning with AS, UNTIL or WHEN,
    • any OF-TYPE speci, and
    • any :GUARD guardi.

    A FOR loop$ expression with just one iteration variable and in which the iterative expressions mention no free variable other than the iteration variable is called a simple loop$ (or, sometimes, a simple loop). An example of a simple loop is

    (loop$ for x in lst when (evenp x) collect (+ 1 (sq x))).

    A FOR loop$ expression is called a fancy loop$ if it is not simple. Both of the following loop$s are fancy.

    (loop$ for x in xlst as y on ylst collect (expr x y))
    
    (loop$ for x in xlst collect (expr x z))

    The first is fancy because it has two iteration variables, x and y. The second is fancy because the body freely uses the variable z which is not the iteration variable.

    Now go to lp-section-5 (or return to the Table of Contents).