		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-lookup-ord

Look up an ordinary identifier in a validation table.

Signature
(valid-lookup-ord ident table) → (mv info? currentp)
Arguments: ident — Guard (identp ident).; table — Guard (valid-tablep table).
Returns: info? — Type (valid-ord-info-optionp info?).; currentp — Type (booleanp currentp).

According to the visibility and hiding rules [C:6.2.1/2], we look up the identifier starting from the innermost scope. We stop as soon as we find a match. We return nil if we reach the outermost scope without finding a match.

We also return a flag saying whether the identifier was found in the current (i.e. innermost) scope or in some other scope. We initialize this flag to t, and we set to nil when we perform the recursive call. The flag is irrelevant if the first result is nil, but in this case the returned flag is nil too.

Definitions and Theorems

Function: valid-lookup-ord-loop

(defun valid-lookup-ord-loop (ident scopes currentp)
  (declare (xargs :guard (and (identp ident)
                              (valid-scope-listp scopes)
                              (booleanp currentp))))
  (let ((__function__ 'valid-lookup-ord-loop))
    (declare (ignorable __function__))
    (b* (((when (endp scopes)) (mv nil nil))
         (scope (car scopes))
         (ord-scope (valid-scope->ord scope))
         (ident+info (assoc-equal (ident-fix ident)
                                  ord-scope))
         ((when ident+info)
          (mv (cdr ident+info)
              (bool-fix currentp))))
      (valid-lookup-ord-loop ident (cdr scopes)
                             nil))))

Theorem: valid-ord-info-optionp-of-valid-lookup-ord-loop.info?

(defthm valid-ord-info-optionp-of-valid-lookup-ord-loop.info?
  (b* (((mv ?info? ?updated-currentp)
        (valid-lookup-ord-loop ident scopes currentp)))
    (valid-ord-info-optionp info?))
  :rule-classes :rewrite)

Theorem: booleanp-of-valid-lookup-ord-loop.updated-currentp

(defthm booleanp-of-valid-lookup-ord-loop.updated-currentp
  (b* (((mv ?info? ?updated-currentp)
        (valid-lookup-ord-loop ident scopes currentp)))
    (booleanp updated-currentp))
  :rule-classes :rewrite)

Theorem: valid-lookup-ord-loop-of-ident-fix-ident

(defthm valid-lookup-ord-loop-of-ident-fix-ident
  (equal (valid-lookup-ord-loop (ident-fix ident)
                                scopes currentp)
         (valid-lookup-ord-loop ident scopes currentp)))

Theorem: valid-lookup-ord-loop-ident-equiv-congruence-on-ident

(defthm valid-lookup-ord-loop-ident-equiv-congruence-on-ident
  (implies
       (ident-equiv ident ident-equiv)
       (equal (valid-lookup-ord-loop ident scopes currentp)
              (valid-lookup-ord-loop ident-equiv scopes currentp)))
  :rule-classes :congruence)

Theorem: valid-lookup-ord-loop-of-valid-scope-list-fix-scopes

(defthm valid-lookup-ord-loop-of-valid-scope-list-fix-scopes
  (equal (valid-lookup-ord-loop ident (valid-scope-list-fix scopes)
                                currentp)
         (valid-lookup-ord-loop ident scopes currentp)))

Theorem: valid-lookup-ord-loop-valid-scope-list-equiv-congruence-on-scopes

(defthm
  valid-lookup-ord-loop-valid-scope-list-equiv-congruence-on-scopes
  (implies
       (valid-scope-list-equiv scopes scopes-equiv)
       (equal (valid-lookup-ord-loop ident scopes currentp)
              (valid-lookup-ord-loop ident scopes-equiv currentp)))
  :rule-classes :congruence)

Theorem: valid-lookup-ord-loop-of-bool-fix-currentp

(defthm valid-lookup-ord-loop-of-bool-fix-currentp
  (equal (valid-lookup-ord-loop ident scopes (bool-fix currentp))
         (valid-lookup-ord-loop ident scopes currentp)))

Theorem: valid-lookup-ord-loop-iff-congruence-on-currentp

(defthm valid-lookup-ord-loop-iff-congruence-on-currentp
  (implies
       (iff currentp currentp-equiv)
       (equal (valid-lookup-ord-loop ident scopes currentp)
              (valid-lookup-ord-loop ident scopes currentp-equiv)))
  :rule-classes :congruence)

Function: valid-lookup-ord

(defun valid-lookup-ord (ident table)
  (declare (xargs :guard (and (identp ident)
                              (valid-tablep table))))
  (let ((__function__ 'valid-lookup-ord))
    (declare (ignorable __function__))
    (valid-lookup-ord-loop ident (valid-table->scopes table)
                           t)))

Theorem: valid-ord-info-optionp-of-valid-lookup-ord.info?

(defthm valid-ord-info-optionp-of-valid-lookup-ord.info?
  (b* (((mv ?info? ?currentp)
        (valid-lookup-ord ident table)))
    (valid-ord-info-optionp info?))
  :rule-classes :rewrite)

Theorem: booleanp-of-valid-lookup-ord.currentp

(defthm booleanp-of-valid-lookup-ord.currentp
  (b* (((mv ?info? ?currentp)
        (valid-lookup-ord ident table)))
    (booleanp currentp))
  :rule-classes :rewrite)

Theorem: valid-lookup-ord-of-ident-fix-ident

(defthm valid-lookup-ord-of-ident-fix-ident
  (equal (valid-lookup-ord (ident-fix ident)
                           table)
         (valid-lookup-ord ident table)))

Theorem: valid-lookup-ord-ident-equiv-congruence-on-ident

(defthm valid-lookup-ord-ident-equiv-congruence-on-ident
  (implies (ident-equiv ident ident-equiv)
           (equal (valid-lookup-ord ident table)
                  (valid-lookup-ord ident-equiv table)))
  :rule-classes :congruence)

Theorem: valid-lookup-ord-of-valid-table-fix-table

(defthm valid-lookup-ord-of-valid-table-fix-table
  (equal (valid-lookup-ord ident (valid-table-fix table))
         (valid-lookup-ord ident table)))

Theorem: valid-lookup-ord-valid-table-equiv-congruence-on-table

(defthm valid-lookup-ord-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-lookup-ord ident table)
                  (valid-lookup-ord ident table-equiv)))
  :rule-classes :congruence)