		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Gen-var-assertions

Generate assertions about certain variables having values of certain types in a computation state.

Signature
(gen-var-assertions vartys compst) → assertions
Arguments: vartys — Guard (c::ident-type-mapp vartys).; compst — An untranslated term.
Returns: assertions — Type (true-listp assertions).

The variables and their types are in the vartys map. For each variable in the map, we generate an assertion saying that the variable can be read from the computation state and it contains a value of the associated type.

The input compst is the (untranslated) term to use for the computation state (often just a variable).

Definitions and Theorems

Function: gen-var-assertions

(defun gen-var-assertions (vartys compst)
  (declare (xargs :guard (c::ident-type-mapp vartys)))
  (let ((__function__ 'gen-var-assertions))
    (declare (ignorable __function__))
    (b* (((when (omap::emptyp (c::ident-type-map-fix vartys)))
          nil)
         ((mv var type) (omap::head vartys))
         (asrt (cons 'c::compustate-has-var-with-type-p
                     (cons (cons 'quote (cons var 'nil))
                           (cons (cons 'quote (cons type 'nil))
                                 (cons compst 'nil)))))
         (asrts (gen-var-assertions (omap::tail vartys)
                                    compst)))
      (cons asrt asrts))))

Theorem: true-listp-of-gen-var-assertions

(defthm true-listp-of-gen-var-assertions
  (b* ((assertions (gen-var-assertions vartys compst)))
    (true-listp assertions))
  :rule-classes :rewrite)

Theorem: gen-var-assertions-of-ident-type-map-fix-vartys

(defthm gen-var-assertions-of-ident-type-map-fix-vartys
  (equal (gen-var-assertions (c::ident-type-map-fix vartys)
                             compst)
         (gen-var-assertions vartys compst)))

Theorem: gen-var-assertions-ident-type-map-equiv-congruence-on-vartys

(defthm gen-var-assertions-ident-type-map-equiv-congruence-on-vartys
  (implies (c::ident-type-map-equiv vartys vartys-equiv)
           (equal (gen-var-assertions vartys compst)
                  (gen-var-assertions vartys-equiv compst)))
  :rule-classes :congruence)