		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-var

Validate a variable.

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

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))))
 (let ((__function__ 'valid-var))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-type) (irr-linkage))
    ((mv info &)
     (valid-lookup-ord var table))
    ((unless info)
     (reterr (msg "The variable ~x0 is not in scope."
                  (ident-fix var))))
    ((unless (valid-ord-info-case info :objfun))
     (reterr
      (msg
       "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)))))

Theorem: typep-of-valid-var.type

(defthm typep-of-valid-var.type
  (b* (((mv acl2::?erp ?type ?linkage)
        (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)
        (valid-var var table)))
    (linkagep linkage))
  :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)