• 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-5

    Informal Semantics of FOR Loop$s

    LP5: Informal Semantics of FOR Loop$s

    The value returned by a FOR loop$ can be specified as follows — but we hasten to add that this is not how Common Lisp compilers implement loop$! We think this description is easier to understand.

    The first step in evaluating a FOR loop$ is to determine the range of each iteration variable by evaluating the target expressions as previously described.

    Next, repeat the following steps until the process stops. (1) If any range is empty, stop. (2) Otherwise, assign each iteration variable the first value in its range and shorten the range by one, by removing that first element. (3) If the until-expr evaluates to non-nil under the current values of the global and iteration variables, stop. Otherwise, if the when-expr evaluates to non-nil under the current values of the variables, then evaluate the body-expr under the current values. Otherwise, do not evaluate the body-expr.

    When the repetition stops, the body-expr will have been evaluated n times, each time producing a value vali, 0 <= i < n, where the vali are listed in the order in which they were produced. The result returned by the loop$ is determined by the operator, op, of the loop$ as follows.

    • SUM          — return the sum of the vali
    • COLLECT — return (LIST val1 ... valn)
    • APPEND   — return (APPEND val1 ... valn)
    • ALWAYS   — return (AND val1 ... valn T)
    • THEREIS — return (OR val1 ... valn)

    Note that if op is ALWAYS, iteration can stop the first time a vali is nil. Similarly, if op is THEREIS, iteration can stop the first time a vali is non-nil. Note also that an ALWAYS loop$ returns NIL or T but a THEREIS loop$ returns nil or the first non-nil value produced by the evaluation of the body.

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