		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Step-from-trans

Evaluation step from a transitional state.

Signature
(step-from-trans stack program) → estate
Arguments: stack — Guard (stackp stack).; program — Guard (programp program).
Returns: estate — Type (eval-state-p estate).

If the stack of frames is empty, we go into an error state. It should be an invariant that the stack is never empty during an evaluation that starts from a suitably well-formed initial state. This will be proved formally eventually.

If the stack is not empty, we pick the top frame, which is the car in our formalization. We look at the term in the frame, which tells us what must be done next.

If the term is a variable, we look it up in the binding of the frame. If the variable is unbounded, we go into an error state; this should never happen in well-formed evaluations, as we plan to prove formally. If it is bounded, we quote the value it is bound to and replace the variable with that quoted constant in the frame. Note that no frame is pushed or popped in this evaluation step in this case.

If the term is not a variable, it is either a quoted constant or a call of a named function or lambda expression. We explain the case of the call first, and then the case of a quoted constant.

If the term is a call of any function other than if (whose treatment is explained later), there are two subcases to consider. The first subcase is that not all the argument terms of the call are quoted constants. In this subcase, we push a new frame with the leftmost argument term that is not a quoted constant; the binding is copied. This is because that, in the left-to-right order of evaluation, that argument is the one that needs to be evaluated next, while the ones that precede it are fully evaluated (i.e. they are quoted constants where no further evaluation is possible). The second subcase is that all the argument terms are quoted constants. In this subcase, all the arguments of the call are fully evaluated (i.e. they are quoted constants where no further evaluation is possible), and so we need to proceed to evaluate the call itself, which we do as follows. If the function is a primitive one, we run it in one step: we use call-primitive-function, and if it returns nil we go into the error state, otherwise we replace the term in the curren frame with the quoted result of the primitive function call. Note that, in this case, the primitive function is never if, because that case would have already been handled non-strictly. If instead the function is a named one that is not primitive, we look up its definition in the program. If no definition is found, we go into the error state; this will never happen in well-formed evaluations, as we plan to prove formally. If a definition is found, we push a new frame with the body of the definition as term, and with a binding that binds the values of the quoted constant arguments to the formal parameters. If instead the function being called is a lambda expression, then we push a new frame with the body of the lambda expression as term and with a binding that extends the current one with the values of the quoted constant arguments bound to the formal parameters. Thus the treatment of the lambda expression is not very different from the treatment of a named function, except that for the latter we need to look up the definition in the program while for the former we already have the ``definition'' right there. Another difference is in the binding in the pushed frame: for a named function, it is a fresh binding, while for a lambda expression, it is an update of the current one. Lambda expressions are closed in ACL2 translated terms, but here we want to be more general, and allow the well-formed evaluation of lambda expressions that are not necessarily closed, as may result, for instance, from transformations of ACL2 terms.

Note that, as just explained, a frame with a call always pushes a new frame, whether it is for the leftmost non-quoted-constant argument of the call, or for the body of the named function or lambda expression called. Successive evaluation steps will operate on the new frame, possibly pushing further frames, and so on, until the originally pushed frame (if the computation terminates) ends up with a quoted constant in it, which is the final result of evaluating the term in the originally pushed frame. This is where a frame with just a quoted constant comes into play, whose treatment we describe next (recall that, above, we had deferred this explanation).

If the term in a frame is a quoted constant, we pop the frame, and incorporate the quoted constant into the frame just below, if any. If there is no frame just below, i.e. the frame with the quoted constant, just popped, was the only one, then we go into the final evaluation state, which only contains a value, namely the value of the quoted constant. This means that the overall computation, which started from an initial evaluation state, has terminated, and this value is the result. If instead there is a frame below, we proceed as follows. If the term in the frame below is a variable or quoted constant, we go into the error state: this will never happen in well-formed evaluations; we will prove this formally eventually. If instead the term is a call, there are two subcases, the same that were described above for pushing a new frame. In the first subcase, the call in the frame has a leftmost argument term that is not a quoted constant: then the frame just popped must have derived from that argument term, and thus we replace that argument term with the quoted constant. In the second subcase, the call in the frame has all quoted constants as arguments: the the frame just popped must have derived from the body of the function, and thus we replace the whole call with the quoted constant.

A call of if is treated non-strictly. If the call has a number of arguments different from 3, we go into an error state; this will never happen in well-formed evaluations, as will be proved eventually. If the first argument (i.e. the test) is not a quoted constant, it is pushed into a new frame, like any other function argument. If instead it is a quoted constant, it means that it has been already evaluated, or that it does not need to be evaluated. Based on whether its value is nil or not, we replace the whole if call with the second or third argument, which we then proceed to evaluate as any other term, in subsequent evaluation steps. Thus, the other branch is completely ignored, not evaluated, realizing the non-strictness of if.

Note that the arguments of functions are evaluated left-to-right. This is consistent with Section 5.1.5 of ``Common Lisp the Language, 2nd Edition''.

Definitions and Theorems

Function: step-from-trans

(defun step-from-trans (stack program)
 (declare (xargs :guard (and (stackp stack)
                             (programp program))))
 (let ((__function__ 'step-from-trans))
  (declare (ignorable __function__))
  (b* (((when (endp stack)) (eval-state-error))
       (frame (car stack))
       ((frame frame) frame))
   (tterm-case
    frame.term :variable
    (b* ((var-val (omap::assoc frame.term.name frame.binding))
         ((unless (consp var-val))
          (eval-state-error))
         (val (cdr var-val))
         (new-frame (change-frame frame
                                  :term (tterm-constant val)))
         (new-stack (cons new-frame (cdr stack))))
      (eval-state-trans new-stack))
    :constant
    (b* ((value frame.term.value)
         (stack (cdr stack))
         ((when (endp stack))
          (eval-state-final value))
         (frame (car stack))
         ((frame frame) frame))
     (tterm-case
      frame.term :variable (eval-state-error)
      :constant (eval-state-error)
      :call
      (b*
       (((mv foundp arguments)
         (put-leftmost-nonconst frame.term.arguments value))
        (term
           (if foundp (make-tterm-call :function frame.term.function
                                       :arguments arguments)
             (tterm-constant value)))
        (frame (change-frame frame :term term))
        (stack (cons frame (cdr stack))))
       (eval-state-trans stack))))
    :call
    (if
     (tfunction-equiv frame.term.function
                      (tfunction-named (lift-symbol 'if)))
     (b* (((unless (= (len frame.term.arguments) 3))
           (eval-state-error))
          (test (first frame.term.arguments)))
      (if (tterm-case test :constant)
          (b* ((branch (if (value-equiv (tterm-constant->value test)
                                        (value-nil))
                           (third frame.term.arguments)
                         (second frame.term.arguments)))
               (new-frame (change-frame frame :term branch))
               (new-stack (cons new-frame (cdr stack))))
            (eval-state-trans new-stack))
        (eval-state-trans (cons (make-frame :term test
                                            :binding frame.binding)
                                stack))))
     (b* ((arg? (get-leftmost-nonconst frame.term.arguments)))
      (if
        (ttermp arg?)
        (eval-state-trans (cons (make-frame :term arg?
                                            :binding frame.binding)
                                stack))
       (tfunction-case
        frame.term.function :named
        (if
         (primitive-function-namep frame.term.function.name)
         (b*
          ((args
             (tterm-constant-list->value-list frame.term.arguments))
           (value? (call-primitive-function
                        frame.term.function.name args program)))
          (if
            (valuep value?)
            (eval-state-trans
                 (cons (change-frame frame
                                     :term (tterm-constant value?))
                       (cdr stack)))
            (eval-state-error)))
         (b*
          ((function?
                (function-lookup frame.term.function.name
                                 (program->functions program)))
           ((unless (functionp function?))
            (eval-state-error))
           (params (function->params function?))
           (body (function->body function?))
           ((unless (= (len params)
                       (len frame.term.arguments)))
            (eval-state-error))
           (args
             (tterm-constant-list->value-list frame.term.arguments))
           (binding (omap::from-lists params args)))
          (eval-state-trans
               (cons (make-frame :term body :binding binding)
                     stack))))
        :lambda
        (b*
         ((params frame.term.function.parameters)
          (body frame.term.function.body)
          ((unless (= (len params)
                      (len frame.term.arguments)))
           (eval-state-error))
          (args
             (tterm-constant-list->value-list frame.term.arguments))
          (binding (omap::update* (omap::from-lists params args)
                                  frame.binding)))
         (eval-state-trans
              (cons (make-frame :term body :binding binding)
                    stack)))))))))))

Theorem: eval-state-p-of-step-from-trans

(defthm eval-state-p-of-step-from-trans
  (b* ((estate (step-from-trans stack program)))
    (eval-state-p estate))
  :rule-classes :rewrite)

Theorem: step-from-trans-of-stack-fix-stack

(defthm step-from-trans-of-stack-fix-stack
  (equal (step-from-trans (stack-fix stack)
                          program)
         (step-from-trans stack program)))

Theorem: step-from-trans-stack-equiv-congruence-on-stack

(defthm step-from-trans-stack-equiv-congruence-on-stack
  (implies (stack-equiv stack stack-equiv)
           (equal (step-from-trans stack program)
                  (step-from-trans stack-equiv program)))
  :rule-classes :congruence)

Theorem: step-from-trans-of-program-fix-program

(defthm step-from-trans-of-program-fix-program
  (equal (step-from-trans stack (program-fix program))
         (step-from-trans stack program)))

Theorem: step-from-trans-program-equiv-congruence-on-program

(defthm step-from-trans-program-equiv-congruence-on-program
  (implies (program-equiv program program-equiv)
           (equal (step-from-trans stack program)
                  (step-from-trans stack program-equiv)))
  :rule-classes :congruence)