Calculate the C types of the formal parameters of a target function.
(atc-typed-formals fn fn-guard prec-tags prec-objs names-to-avoid wrld) → (mv erp typed-formals events updated-names-to-avoid)
We look for conjuncts from which we derive,
according to atc-check-guard-conjunct,
types for the formals of
We also generate theorems about the formals.
If we find types for all the formals, we return an alist from the formals to their variable information. The alist has unique keys, in the order of the formals.
We first extract the guard's conjuncts, then we go through the conjuncts, looking for the pattern, and we extend an alist from formals to types as we find patterns; this preliminary alist may not have the keys in order, because it goes according to the order of the guard's conjuncts. As we construct this preliminary alist, we check for multiple terms for the same formal, rejecting them even if they are identical. Then we construct the final alist by going through the formals in order, and looking up their types in the preliminary alist; here we detect when a formal has no corresponding conjunct in the guard.
We also consult the defobject alist
to set the
Function:
(defun atc-typed-formals-prelim-alist (fn fn-guard formals guard guard-conjuncts prec-tags prec-objs names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (symbol-listp formals) (pseudo-termp guard) (pseudo-term-listp guard-conjuncts) (atc-string-taginfo-alistp prec-tags) (atc-string-objinfo-alistp prec-objs) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-typed-formals-prelim-alist)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil) ((when (endp guard-conjuncts)) (retok nil nil names-to-avoid)) (conjunct (car guard-conjuncts)) ((mv type defobj-pred arg) (atc-check-guard-conjunct conjunct prec-tags prec-objs)) ((unless type) (atc-typed-formals-prelim-alist fn fn-guard formals guard (cdr guard-conjuncts) prec-tags prec-objs names-to-avoid wrld)) ((unless (member-eq arg formals)) (atc-typed-formals-prelim-alist fn fn-guard formals guard (cdr guard-conjuncts) prec-tags prec-objs names-to-avoid wrld)) ((erp prelim-alist events names-to-avoid) (atc-typed-formals-prelim-alist fn fn-guard formals guard (cdr guard-conjuncts) prec-tags prec-objs names-to-avoid wrld)) ((when (consp (assoc-eq arg prelim-alist))) (reterr (msg "The guard ~x0 of the target function ~x1 ~ includes multiple type predicates ~ for the formal parameter ~x2. ~ This is disallowed: every formal parameter ~ must have exactly one type predicate in the guard, ~ even when the multiple predicates are the same." guard fn arg))) ((mv event name names-to-avoid) (atc-gen-formal-thm fn fn-guard formals arg type defobj-pred prec-tags names-to-avoid wrld)) (events (cons event events)) (externalp (b* ((info? (cdr (assoc-equal (symbol-name arg) prec-objs)))) (and info? t))) (info (make-atc-var-info :type type :thm name :externalp externalp)) (prelim-alist (acons arg info prelim-alist))) (retok prelim-alist events names-to-avoid))))
Theorem:
(defthm atc-symbol-varinfo-alistp-of-atc-typed-formals-prelim-alist.prelim-alist-final (b* (((mv acl2::?erp ?prelim-alist-final ?events ?updated-names-to-avoid) (atc-typed-formals-prelim-alist fn fn-guard formals guard guard-conjuncts prec-tags prec-objs names-to-avoid wrld))) (atc-symbol-varinfo-alistp prelim-alist-final)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-typed-formals-prelim-alist.events (b* (((mv acl2::?erp ?prelim-alist-final ?events ?updated-names-to-avoid) (atc-typed-formals-prelim-alist fn fn-guard formals guard guard-conjuncts prec-tags prec-objs names-to-avoid wrld))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-typed-formals-prelim-alist.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv acl2::?erp ?prelim-alist-final ?events ?updated-names-to-avoid) (atc-typed-formals-prelim-alist fn fn-guard formals guard guard-conjuncts prec-tags prec-objs names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)
Function:
(defun atc-typed-formals-final-alist (fn formals guard prelim-alist wrld) (declare (xargs :guard (and (symbolp fn) (symbol-listp formals) (pseudo-termp guard) (atc-symbol-varinfo-alistp prelim-alist) (plist-worldp wrld)))) (let ((__function__ 'atc-typed-formals-final-alist)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (endp formals)) (retok nil)) (formal (car formals)) (formal (mbe :logic (symbol-fix formal) :exec formal)) (formal+info (assoc-eq formal (atc-symbol-varinfo-alist-fix prelim-alist))) ((when (not (consp formal+info))) (reterr (msg "The guard ~x0 of the target function ~x1 ~ has no type predicate for the formal parameter ~x2. ~ Every formal parameter must have a type predicate." guard fn formal))) (info (cdr formal+info)) ((erp typed-formals) (atc-typed-formals-final-alist fn (cdr formals) guard prelim-alist wrld))) (retok (acons formal info typed-formals)))))
Theorem:
(defthm atc-symbol-varinfo-alistp-of-atc-typed-formals-final-alist.typed-formals (b* (((mv acl2::?erp ?typed-formals) (atc-typed-formals-final-alist fn formals guard prelim-alist wrld))) (atc-symbol-varinfo-alistp typed-formals)) :rule-classes :rewrite)
Function:
(defun atc-typed-formals (fn fn-guard prec-tags prec-objs names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (atc-string-taginfo-alistp prec-tags) (atc-string-objinfo-alistp prec-objs) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-typed-formals)) (declare (ignorable __function__)) (b* (((reterr) nil nil nil) (formals (formals+ fn wrld)) (guard (uguard+ fn wrld)) (guard-conjuncts (flatten-ands-in-lit guard)) ((erp prelim-alist events names-to-avoid) (atc-typed-formals-prelim-alist fn fn-guard formals guard guard-conjuncts prec-tags prec-objs names-to-avoid wrld)) ((erp typed-formals) (atc-typed-formals-final-alist fn formals guard prelim-alist wrld))) (retok typed-formals events names-to-avoid))))
Theorem:
(defthm atc-symbol-varinfo-alistp-of-atc-typed-formals.typed-formals (b* (((mv acl2::?erp ?typed-formals ?events ?updated-names-to-avoid) (atc-typed-formals fn fn-guard prec-tags prec-objs names-to-avoid wrld))) (atc-symbol-varinfo-alistp typed-formals)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-typed-formals.events (b* (((mv acl2::?erp ?typed-formals ?events ?updated-names-to-avoid) (atc-typed-formals fn fn-guard prec-tags prec-objs names-to-avoid wrld))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-typed-formals.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv acl2::?erp ?typed-formals ?events ?updated-names-to-avoid) (atc-typed-formals fn fn-guard prec-tags prec-objs names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)