		Search-engine friendly clone of the ACL2 documentation.

Atc-generation-contexts

Atc-contextualize

Put a formula into a context.

Signature
(atc-contextualize formula context fn? fn-guard? compst-var? limit-var? limit-bound? preamblep wrld) → formula1
Arguments: formula — An untranslated term.; context — Guard (atc-contextp context).; fn? — Guard (symbolp fn?).; fn-guard? — Guard (symbolp fn-guard?).; compst-var? — Guard (symbolp compst-var?).; limit-var? — Guard (symbolp limit-var?).; limit-bound? — Guard (pseudo-termp limit-bound?).; preamblep — Guard (booleanp preamblep).; wrld — Guard (plist-worldp wrld).
Returns: formula1 — An untranslated term.

We go through the context elements, generating code for them and ending with the term given as input.

We also add, around the resulting term from the process described above, additional premises:

The fact that the computation state variable is a computation state.
The preamble from the context.
The fact that the guard of the target function fn holds on the formals of the function.
The fact that the limit variable is an integer.
The fact that the limit variable is greater than or equal to a given bound (expressed as a term).

If preamblep is nil, we omit the preamble from the context. This is used to generate some claims within the ACL2 proof builder.

If fn-guard? is nil, we omit the guard hypothesis. This is used to generate some claims within the ACL2 proof builder. In this case, fn? must be nil too.

If compst-var? is nil, we avoid all the premises and hypotheses that concern computation states. Some of the theorems we generate do not involve computation states: they apply just to ACL2 terms that represent shallowly embedded C code; they do not apply to relations between ACL2 terms and deeply embedded C code.

If limit-var? is nil, we avoid the hypotheses that concern limits. Some of the theorems we generate (e.g. for pure expressions) do not involve execution recursion limits. In this case, limit-bound? must be nil too.

Definitions and Theorems

Function: atc-contextualize-aux

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

Function: atc-contextualize

(defun atc-contextualize
       (formula context fn? fn-guard? compst-var?
                limit-var? limit-bound? preamblep wrld)
 (declare (xargs :guard (and (atc-contextp context)
                             (symbolp fn?)
                             (symbolp fn-guard?)
                             (symbolp compst-var?)
                             (symbolp limit-var?)
                             (pseudo-termp limit-bound?)
                             (booleanp preamblep)
                             (plist-worldp wrld))))
 (let ((__function__ 'atc-contextualize))
  (declare (ignorable __function__))
  (b*
   ((skip-cs (not compst-var?))
    (formula
      (atc-contextualize-aux formula (atc-context->premises context)
                             skip-cs))
    (hyps
     (append
      (and compst-var?
           (cons (cons 'compustatep
                       (cons compst-var? 'nil))
                 'nil))
      (and preamblep
           (atc-context->preamble context))
      (and fn-guard?
           (cons (cons fn-guard? (formals+ fn? wrld))
                 'nil))
      (and
       limit-var?
       (cons (cons 'integerp (cons limit-var? 'nil))
             (cons (cons '>=
                         (cons limit-var? (cons limit-bound? 'nil)))
                   'nil)))))
    ((when (and (not fn-guard?) fn?))
     (raise "Internal error: FN-GUARD? is NIL but FN? is ~x0."
            fn?))
    ((when (and (not limit-var?) limit-bound?))
     (raise
        "Internal error: LIMIT-VAR? is NIL but LIMIT-BOUND? is ~x0."
        limit-bound?))
    (formula (cons 'implies
                   (cons (cons 'and hyps)
                         (cons formula 'nil)))))
   formula)))