Generate a type formula for a term.
(atc-gen-term-type-formula uterm type affect inscope prec-tags) → (mv formula thm-names)
Each ACL2 term translated to C returns 0 or 1 C values and affects 0 or more C objects: the returned C value (if any) and the affected C objects are represented by the ACL2 values returned by the term. (So if the term returns 0 C values, it must affect at least one C object, because terms always return at least one ACL2 value.) Each value returned by the term has a C type, which has a corresponding ACL2 recognizer. Here we return a formula that is a conjunction of assertions, one per value returned by the term, which applies the associated recognizer to the corresponding term's result.
For each array value returned by the term, we also return, as part of the formula, an assertion saying that the length of the array is the same as the corresponding variable. Since a C array type is described by both the element type and the size, it makes sense that assertions about the length accompany assertions involving the recognizers (which only talk about the element type). These assertions are not generated when they would lead to rewrite rules that rewrite a term to itself, which are illegal rewrite rules; the exact circumstances are explained below.
We also return the names of the theorems from the symbol table that are associated to each variable for the affected objects. These are used to prove the formula returned here.
We go through the
Function:
(defun atc-gen-type-formulas-aux1 (affect inscope) (declare (xargs :guard (and (symbol-listp affect) (atc-symbol-varinfo-alist-listp inscope)))) (let ((__function__ 'atc-gen-type-formulas-aux1)) (declare (ignorable __function__)) (b* (((when (endp affect)) (mv nil nil)) (var (car affect)) (info (atc-get-var var inscope)) ((unless info) (raise "Internal error: no information for variable ~x0." var) (mv nil nil)) (type (atc-var-info->type info)) (thm-name (atc-var-info->thm info)) ((mv more-types more-thm-names) (atc-gen-type-formulas-aux1 (cdr affect) inscope))) (mv (cons type more-types) (cons thm-name more-thm-names)))))
Theorem:
(defthm type-listp-of-atc-gen-type-formulas-aux1.types (b* (((mv ?types ?thm-names) (atc-gen-type-formulas-aux1 affect inscope))) (type-listp types)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-type-formulas-aux1.thm-names (b* (((mv ?types ?thm-names) (atc-gen-type-formulas-aux1 affect inscope))) (symbol-listp thm-names)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-atc-gen-type-formulas-aux1.types (b* (((mv ?types ?thm-names) (atc-gen-type-formulas-aux1 affect inscope))) (true-listp types)) :rule-classes :type-prescription)
Function:
(defun atc-gen-type-formulas-aux2 (types uterms varps bound-vars affected-vars prec-tags) (declare (xargs :guard (and (type-listp types) (true-listp uterms) (boolean-listp varps) (symbol-listp bound-vars) (symbol-listp affected-vars) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-gen-type-formulas-aux2)) (declare (ignorable __function__)) (b* (((when (endp types)) nil) (type (car types)) (uterm (car uterms)) (affected-var (car affected-vars)) (pred (atc-type-to-recognizer type prec-tags)) (conjuncts (if (type-case type :array) (b* ((elemtype (type-array->of type)) (elemfixtype (type-kind elemtype)) (array-length (pack elemfixtype '-array-length))) (cons (cons pred (cons uterm 'nil)) (and (or (not (car varps)) (member-eq affected-var bound-vars)) (cons (cons 'equal (cons (cons array-length (cons uterm 'nil)) (cons (cons array-length (cons affected-var 'nil)) 'nil))) 'nil)))) (cons (cons pred (cons uterm 'nil)) 'nil))) (more-conjuncts (atc-gen-type-formulas-aux2 (cdr types) (cdr uterms) (cdr varps) bound-vars (cdr affected-vars) prec-tags))) (append conjuncts more-conjuncts))))
Theorem:
(defthm true-listp-of-atc-gen-type-formulas-aux2 (b* ((conjuncts (atc-gen-type-formulas-aux2 types uterms varps bound-vars affected-vars prec-tags))) (true-listp conjuncts)) :rule-classes :rewrite)
Function:
(defun atc-gen-term-type-formula (uterm type affect inscope prec-tags) (declare (xargs :guard (and (typep type) (symbol-listp affect) (atc-symbol-varinfo-alist-listp inscope) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-gen-term-type-formula)) (declare (ignorable __function__)) (b* (((mv affect-types thm-names) (atc-gen-type-formulas-aux1 affect inscope)) (types (if (type-case type :void) affect-types (cons type affect-types))) ((when (endp types)) (raise "Internal error: term ~x0 returns no values." uterm) (mv nil nil)) ((mv uterms varps bound-vars) (atc-uterm-to-components uterm (len types))) (conjuncts (atc-gen-type-formulas-aux2 types uterms varps bound-vars (if (type-case type :void) affect (cons nil affect)) prec-tags)) (formula (if (endp (cdr conjuncts)) (car conjuncts) (cons 'and conjuncts)))) (mv formula thm-names))))
Theorem:
(defthm symbol-listp-of-atc-gen-term-type-formula.thm-names (b* (((mv acl2::?formula ?thm-names) (atc-gen-term-type-formula uterm type affect inscope prec-tags))) (symbol-listp thm-names)) :rule-classes :rewrite)