		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-vartys-from-valid-table

Generate, from a validation table, a map from identifiers to types.

Signature
(simpadd0-vartys-from-valid-table table) → vatys
Arguments: table — Guard (c$::valid-tablep table).
Returns: vatys — Type (ident-type-mapp vatys).

The validation table is from validation annotations. The resulting map contains all the variables in scope whose types satisfy type-formalp; variables of other types are skipped. Given that later scopes may contain variables that shadow earlier scopes, we process the scopes in the validation table from oldest to newest, overriding map entries as applicable.

Definitions and Theorems

Function: simpadd0-vartys-from-valid-ord-scope

(defun simpadd0-vartys-from-valid-ord-scope (oscope)
 (declare (xargs :guard (c$::valid-ord-scopep oscope)))
 (let ((__function__ 'simpadd0-vartys-from-valid-ord-scope))
   (declare (ignorable __function__))
   (b* (((when (endp oscope)) nil)
        ((cons ident info) (car oscope))
        (vartys (simpadd0-vartys-from-valid-ord-scope (cdr oscope)))
        ((unless (c$::valid-ord-info-case info :objfun))
         vartys)
        (type (c$::valid-ord-info-objfun->type info))
        ((unless (type-formalp type)) vartys))
     (omap::update ident type vartys))))

Theorem: ident-type-mapp-of-simpadd0-vartys-from-valid-ord-scope

(defthm ident-type-mapp-of-simpadd0-vartys-from-valid-ord-scope
  (implies
       (and (c$::valid-ord-scopep oscope))
       (b* ((vartys (simpadd0-vartys-from-valid-ord-scope oscope)))
         (ident-type-mapp vartys)))
  :rule-classes :rewrite)

Function: simpadd0-vartys-from-valid-scope

(defun simpadd0-vartys-from-valid-scope (scope)
  (declare (xargs :guard (c$::valid-scopep scope)))
  (let ((__function__ 'simpadd0-vartys-from-valid-scope))
    (declare (ignorable __function__))
    (simpadd0-vartys-from-valid-ord-scope
         (c$::valid-scope->ord scope))))

Theorem: ident-type-mapp-of-simpadd0-vartys-from-valid-scope

(defthm ident-type-mapp-of-simpadd0-vartys-from-valid-scope
  (b* ((vartys (simpadd0-vartys-from-valid-scope scope)))
    (ident-type-mapp vartys))
  :rule-classes :rewrite)

Function: simpadd0-vartys-from-valid-scope-list

(defun simpadd0-vartys-from-valid-scope-list (scopes)
 (declare (xargs :guard (c$::valid-scope-listp scopes)))
 (let ((__function__ 'simpadd0-vartys-from-valid-scope-list))
  (declare (ignorable __function__))
  (cond ((endp scopes) nil)
        (t (omap::update*
                (simpadd0-vartys-from-valid-scope-list (cdr scopes))
                (simpadd0-vartys-from-valid-scope (car scopes)))))))

Theorem: ident-type-mapp-of-simpadd0-vartys-from-valid-scope-list

(defthm ident-type-mapp-of-simpadd0-vartys-from-valid-scope-list
  (implies
       (and (c$::valid-scope-listp scopes))
       (b* ((vartys (simpadd0-vartys-from-valid-scope-list scopes)))
         (ident-type-mapp vartys)))
  :rule-classes :rewrite)

Function: simpadd0-vartys-from-valid-table

(defun simpadd0-vartys-from-valid-table (table)
  (declare (xargs :guard (c$::valid-tablep table)))
  (let ((__function__ 'simpadd0-vartys-from-valid-table))
    (declare (ignorable __function__))
    (simpadd0-vartys-from-valid-scope-list
         (c$::valid-table->scopes table))))

Theorem: ident-type-mapp-of-simpadd0-vartys-from-valid-table

(defthm ident-type-mapp-of-simpadd0-vartys-from-valid-table
  (b* ((vatys (simpadd0-vartys-from-valid-table table)))
    (ident-type-mapp vatys))
  :rule-classes :rewrite)