		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-var

Validate a variable.

Signature
(valid-var var table) → (mv erp type linkage uid)
Arguments: var — Guard (identp var).; table — Guard (valid-tablep table).
Returns: erp — Type (maybe-msgp erp).; type — Type (typep type).; linkage — Type (linkagep linkage).; uid — Type (uidp uid).

This is used to validate the :ident case of the expr fixtype. This is the case of a variable, not an enumeration constant, which is part of the :const case of expr. Recall that the parser initially parses all identifiers used as expressions under the :ident case, but the disambiguator re-classifies some of them under the :const case, as appropriate.

A variable (i.e. identifier) is valid if it is found in the validation table, recorded as denoting an object or function [C17:6.5.1/2]. The type and the linkage are obtained from the table.

Definitions and Theorems

Function: valid-var

(defun valid-var (var table)
 (declare (xargs :guard (and (identp var)
                             (valid-tablep table))))
 (b*
  (((reterr)
    (irr-type)
    (irr-linkage)
    (irr-uid))
   ((mv info &)
    (valid-lookup-ord var table))
   ((unless info)
    (retmsg$ "The variable ~x0 is not in scope."
             (ident-fix var)))
   ((unless (valid-ord-info-case info :objfun))
    (retmsg$
     "The identifier ~x0, used as a variable,is in scope, ~
                  but does not denote an object or function."
     (ident-fix var))))
  (retok (valid-ord-info-objfun->type info)
         (valid-ord-info-objfun->linkage info)
         (valid-ord-info-objfun->uid info))))

Theorem: maybe-msgp-of-valid-var.erp

(defthm maybe-msgp-of-valid-var.erp
  (b* (((mv acl2::?erp ?type ?linkage ?uid)
        (valid-var var table)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-var.type

(defthm typep-of-valid-var.type
  (b* (((mv acl2::?erp ?type ?linkage ?uid)
        (valid-var var table)))
    (typep type))
  :rule-classes :rewrite)

Theorem: linkagep-of-valid-var.linkage

(defthm linkagep-of-valid-var.linkage
  (b* (((mv acl2::?erp ?type ?linkage ?uid)
        (valid-var var table)))
    (linkagep linkage))
  :rule-classes :rewrite)

Theorem: uidp-of-valid-var.uid

(defthm uidp-of-valid-var.uid
  (b* (((mv acl2::?erp ?type ?linkage ?uid)
        (valid-var var table)))
    (uidp uid))
  :rule-classes :rewrite)

Theorem: valid-var-of-ident-fix-var

(defthm valid-var-of-ident-fix-var
  (equal (valid-var (ident-fix var) table)
         (valid-var var table)))

Theorem: valid-var-ident-equiv-congruence-on-var

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

Theorem: valid-var-of-valid-table-fix-table

(defthm valid-var-of-valid-table-fix-table
  (equal (valid-var var (valid-table-fix table))
         (valid-var var table)))

Theorem: valid-var-valid-table-equiv-congruence-on-table

(defthm valid-var-valid-table-equiv-congruence-on-table
  (implies (valid-table-equiv table table-equiv)
           (equal (valid-var var table)
                  (valid-var var table-equiv)))
  :rule-classes :congruence)