		Search-engine friendly clone of the ACL2 documentation.

Atc-generation-contexts

Atc-contextualize-compustate

Put a computation state into a context that is the difference between two contexts.

Signature
(atc-contextualize-compustate compst-var context-start context-end) → term
Arguments: compst-var — Guard (symbolp compst-var).; context-start — Guard (atc-contextp context-start).; context-end — Guard (atc-contextp context-end).
Returns: term — An untranslated term.

When generating modular proofs, in certain cases we need to contextualize the computation state to the ``difference'' between a starting context and an ending context, where the latter is an extension of the former. This ACL2 function accomplished this.

The initial computation state is expressed as a variable, passed to this ACL2 function as compst-var.

We ensure that the starting context is a prefix of the ending context, i.e. it has the same preamble and a prefix of the premises. This should be always the case when this ACL2 function is called, but we defensively check that, stopping with an error if the check fails.

We calculate the premises in the ending context that are not in the starting context, and we go through them, wrapping the computation state variable with lets corresponding to binding of computation states and C variables.

We skip any test encountered in the list of premises. Because of the way this function is used, this is adeguate. The context difference may include tests in modular proofs, so it would be inappropriate to stop with an error upon encountering a test here.

Definitions and Theorems

Function: atc-contextualize-compustate-aux

(defun atc-contextualize-compustate-aux (compst-var premises)
 (declare (xargs :guard (and (symbolp compst-var)
                             (atc-premise-listp premises))))
 (let ((__function__ 'atc-contextualize-compustate-aux))
  (declare (ignorable __function__))
  (b* (((when (endp premises)) compst-var)
       (premise (car premises)))
   (atc-premise-case
    premise
    :compustate
    (cons
     'let
     (cons
      (cons (cons premise.var (cons premise.term 'nil))
            'nil)
      (cons
        (atc-contextualize-compustate-aux compst-var (cdr premises))
        'nil)))
    :cvalue
    (cons
     'let
     (cons
      (cons (cons premise.var (cons premise.term 'nil))
            'nil)
      (cons
        (atc-contextualize-compustate-aux compst-var (cdr premises))
        'nil)))
    :cvalues
    (cons
     'mv-let
     (cons
      premise.vars
      (cons
       premise.term
       (cons
        (atc-contextualize-compustate-aux compst-var (cdr premises))
        'nil))))
    :test
    (atc-contextualize-compustate-aux compst-var (cdr premises))))))

Function: atc-contextualize-compustate

(defun atc-contextualize-compustate
       (compst-var context-start context-end)
 (declare (xargs :guard (and (symbolp compst-var)
                             (atc-contextp context-start)
                             (atc-contextp context-end))))
 (let ((__function__ 'atc-contextualize-compustate))
  (declare (ignorable __function__))
  (b*
   (((unless (equal (atc-context->preamble context-start)
                    (atc-context->preamble context-end)))
     (raise
          "Internal error: different context preambles ~x0 and ~x1."
          (atc-context->preamble context-start)
          (atc-context->preamble context-end)))
    (premises-start (atc-context->premises context-start))
    (premises-end (atc-context->premises context-end))
    ((unless (prefixp premises-start premises-end))
     (raise
        "Internal error: premises ~x0 not a prefix of premises ~x1."
        premises-start premises-end))
    (premises-diff (nthcdr (len premises-start)
                           premises-end)))
   (atc-contextualize-compustate-aux compst-var premises-diff))))