		Search-engine friendly clone of the ACL2 documentation.

Atc-variable-tables

Atc-check-var

Check a variable against a symbol table.

Signature
(atc-check-var var inscope) → (mv info? innermostp errorp)
Arguments: var — Guard (symbolp var).; inscope — Guard (atc-symbol-varinfo-alist-listp inscope).
Returns: info? — Type (atc-var-info-optionp info?).; innermostp — Type (booleanp innermostp).; errorp — Type (booleanp errorp).

If the variable is in the symbol table, we return its information, along with a flag indicating whether the variable is in the innermost scope. If the symbol table contains a different variable with the same symbol name, we return an indication of error; this is because ACL2 variables represent C variables whose names are just the symbol names of the ACL2 variables, which therefore must be distinct for different ACL2 variables.

It is an invariant that all the variables in the symbol table have distinct symbol names.

Definitions and Theorems

Function: atc-check-var-aux

(defun atc-check-var-aux (var inscope innermostp)
 (declare
      (xargs :guard (and (symbolp var)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (booleanp innermostp))))
 (let ((__function__ 'atc-check-var-aux))
  (declare (ignorable __function__))
  (b* (((when (endp inscope)) (mv nil nil nil))
       (scope (car inscope))
       (info? (cdr (assoc-eq var
                             (atc-symbol-varinfo-alist-fix scope))))
       ((when info?) (mv info? innermostp nil))
       ((when (member-equal (symbol-name var)
                            (symbol-name-lst (strip-cars scope))))
        (mv nil nil t)))
    (atc-check-var-aux var (cdr inscope)
                       nil))))

Theorem: atc-var-info-optionp-of-atc-check-var-aux.info?

(defthm atc-var-info-optionp-of-atc-check-var-aux.info?
  (b* (((mv ?info? ?innermostp ?errorp)
        (atc-check-var-aux var inscope innermostp)))
    (atc-var-info-optionp info?))
  :rule-classes :rewrite)

Theorem: booleanp-of-atc-check-var-aux.innermostp

(defthm booleanp-of-atc-check-var-aux.innermostp
  (implies (booleanp innermostp)
           (b* (((mv ?info? ?innermostp ?errorp)
                 (atc-check-var-aux var inscope innermostp)))
             (booleanp innermostp)))
  :rule-classes :rewrite)

Theorem: booleanp-of-atc-check-var-aux.errorp

(defthm booleanp-of-atc-check-var-aux.errorp
  (b* (((mv ?info? ?innermostp ?errorp)
        (atc-check-var-aux var inscope innermostp)))
    (booleanp errorp))
  :rule-classes :rewrite)

Function: atc-check-var

(defun atc-check-var (var inscope)
 (declare
      (xargs :guard (and (symbolp var)
                         (atc-symbol-varinfo-alist-listp inscope))))
 (let ((__function__ 'atc-check-var))
   (declare (ignorable __function__))
   (atc-check-var-aux var inscope t)))

Theorem: atc-var-info-optionp-of-atc-check-var.info?

(defthm atc-var-info-optionp-of-atc-check-var.info?
  (b* (((mv ?info? ?innermostp ?errorp)
        (atc-check-var var inscope)))
    (atc-var-info-optionp info?))
  :rule-classes :rewrite)

Theorem: booleanp-of-atc-check-var.innermostp

(defthm booleanp-of-atc-check-var.innermostp
  (b* (((mv ?info? ?innermostp ?errorp)
        (atc-check-var var inscope)))
    (booleanp innermostp))
  :rule-classes :rewrite)

Theorem: booleanp-of-atc-check-var.errorp

(defthm booleanp-of-atc-check-var.errorp
  (b* (((mv ?info? ?innermostp ?errorp)
        (atc-check-var var inscope)))
    (booleanp errorp))
  :rule-classes :rewrite)