Verified clause-processor for extracting type declarations
Theorem:
(defthm ev-extract-constraint-0 (implies (and (consp acl2::x) (syntaxp (not (equal acl2::a ''nil))) (not (equal (car acl2::x) 'quote))) (equal (ev-extract acl2::x acl2::a) (ev-extract (cons (car acl2::x) (kwote-lst (ev-lst-extract (cdr acl2::x) acl2::a))) nil))))
Theorem:
(defthm ev-extract-constraint-1 (implies (symbolp acl2::x) (equal (ev-extract acl2::x acl2::a) (and acl2::x (cdr (assoc-equal acl2::x acl2::a))))))
Theorem:
(defthm ev-extract-constraint-2 (implies (and (consp acl2::x) (equal (car acl2::x) 'quote)) (equal (ev-extract acl2::x acl2::a) (cadr acl2::x))))
Theorem:
(defthm ev-extract-constraint-3 (implies (and (consp acl2::x) (consp (car acl2::x))) (equal (ev-extract acl2::x acl2::a) (ev-extract (caddr (car acl2::x)) (pairlis$ (cadr (car acl2::x)) (ev-lst-extract (cdr acl2::x) acl2::a))))))
Theorem:
(defthm ev-extract-constraint-4 (implies (not (consp acl2::x-lst)) (equal (ev-lst-extract acl2::x-lst acl2::a) nil)))
Theorem:
(defthm ev-extract-constraint-5 (implies (consp acl2::x-lst) (equal (ev-lst-extract acl2::x-lst acl2::a) (cons (ev-extract (car acl2::x-lst) acl2::a) (ev-lst-extract (cdr acl2::x-lst) acl2::a)))))
Theorem:
(defthm ev-extract-constraint-6 (implies (and (not (consp acl2::x)) (not (symbolp acl2::x))) (equal (ev-extract acl2::x acl2::a) nil)))
Theorem:
(defthm ev-extract-constraint-7 (implies (and (consp acl2::x) (not (consp (car acl2::x))) (not (symbolp (car acl2::x)))) (equal (ev-extract acl2::x acl2::a) nil)))
Theorem:
(defthm ev-extract-constraint-8 (implies (and (consp acl2::x) (equal (car acl2::x) 'not)) (equal (ev-extract acl2::x acl2::a) (not (ev-extract (cadr acl2::x) acl2::a)))))
Theorem:
(defthm ev-extract-constraint-9 (implies (and (consp acl2::x) (equal (car acl2::x) 'if)) (equal (ev-extract acl2::x acl2::a) (if (ev-extract (cadr acl2::x) acl2::a) (ev-extract (caddr acl2::x) acl2::a) (ev-extract (cadddr acl2::x) acl2::a)))))
Theorem:
(defthm ev-extract-constraint-10 (implies (and (consp acl2::x) (equal (car acl2::x) 'implies)) (equal (ev-extract acl2::x acl2::a) (implies (ev-extract (cadr acl2::x) acl2::a) (ev-extract (caddr acl2::x) acl2::a)))))
Theorem:
(defthm ev-extract-constraint-11 (implies (and (consp acl2::x) (equal (car acl2::x) 'hint-please)) (equal (ev-extract acl2::x acl2::a) (hint-please (ev-extract (cadr acl2::x) acl2::a)))))
Theorem:
(defthm ev-extract-disjoin-cons (iff (ev-extract (disjoin (cons acl2::x acl2::y)) acl2::a) (or (ev-extract acl2::x acl2::a) (ev-extract (disjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-extract-disjoin-when-consp (implies (consp acl2::x) (iff (ev-extract (disjoin acl2::x) acl2::a) (or (ev-extract (car acl2::x) acl2::a) (ev-extract (disjoin (cdr acl2::x)) acl2::a)))))
Theorem:
(defthm ev-extract-disjoin-atom (implies (not (consp acl2::x)) (equal (ev-extract (disjoin acl2::x) acl2::a) nil)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm ev-extract-disjoin-append (iff (ev-extract (disjoin (append acl2::x acl2::y)) acl2::a) (or (ev-extract (disjoin acl2::x) acl2::a) (ev-extract (disjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-extract-conjoin-cons (iff (ev-extract (conjoin (cons acl2::x acl2::y)) acl2::a) (and (ev-extract acl2::x acl2::a) (ev-extract (conjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-extract-conjoin-when-consp (implies (consp acl2::x) (iff (ev-extract (conjoin acl2::x) acl2::a) (and (ev-extract (car acl2::x) acl2::a) (ev-extract (conjoin (cdr acl2::x)) acl2::a)))))
Theorem:
(defthm ev-extract-conjoin-atom (implies (not (consp acl2::x)) (equal (ev-extract (conjoin acl2::x) acl2::a) t)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm ev-extract-conjoin-append (iff (ev-extract (conjoin (append acl2::x acl2::y)) acl2::a) (and (ev-extract (conjoin acl2::x) acl2::a) (ev-extract (conjoin acl2::y) acl2::a))))
Theorem:
(defthm ev-extract-conjoin-clauses-cons (iff (ev-extract (conjoin-clauses (cons acl2::x acl2::y)) acl2::a) (and (ev-extract (disjoin acl2::x) acl2::a) (ev-extract (conjoin-clauses acl2::y) acl2::a))))
Theorem:
(defthm ev-extract-conjoin-clauses-when-consp (implies (consp acl2::x) (iff (ev-extract (conjoin-clauses acl2::x) acl2::a) (and (ev-extract (disjoin (car acl2::x)) acl2::a) (ev-extract (conjoin-clauses (cdr acl2::x)) acl2::a)))))
Theorem:
(defthm ev-extract-conjoin-clauses-atom (implies (not (consp acl2::x)) (equal (ev-extract (conjoin-clauses acl2::x) acl2::a) t)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm ev-extract-conjoin-clauses-append (iff (ev-extract (conjoin-clauses (append acl2::x acl2::y)) acl2::a) (and (ev-extract (conjoin-clauses acl2::x) acl2::a) (ev-extract (conjoin-clauses acl2::y) acl2::a))))
Function:
(defun type-extract-helper (cl smtlink-hint state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-term-listp cl) (smtlink-hint-p smtlink-hint)))) (let ((acl2::__function__ 'type-extract-helper)) (declare (ignorable acl2::__function__)) (b* ((cl (pseudo-term-list-fix cl)) (smtlink-hint (smtlink-hint-fix smtlink-hint)) ((smtlink-hint h) smtlink-hint) (g (disjoin cl)) ((mv type-decl-list g/type) (smt-extract g h.fty-info h.abs)) ((mv err type-decl-list-translated) (acl2::translate-cmp (cons 'list type-decl-list) t t nil 'type-extract-cp->type-extract-helper (w state) (default-state-vars t))) ((when err) (er hard? 'type-extract-cp->type-extract-helper "Error ~ translating form: ~@0" (cons 'list type-decl-list)))) (change-smtlink-hint h :expanded-g/type g/type :type-decl-list type-decl-list-translated))))
Function:
(defun type-extract-fn (cl smtlink-hint) (declare (xargs :guard (pseudo-term-listp cl))) (let ((acl2::__function__ 'type-extract-fn)) (declare (ignorable acl2::__function__)) (b* (((unless (pseudo-term-listp cl)) nil) ((unless (smtlink-hint-p smtlink-hint)) (list cl)) ((smtlink-hint h) smtlink-hint) (g (disjoin cl)) (type-decl-list h.type-decl-list) (g/type h.expanded-g/type) (next-cp (cdr (assoc-equal 'type-extract *smt-architecture*))) ((if (null next-cp)) (list cl)) (the-hint (cons ':clause-processor (cons (cons next-cp (cons 'clause (cons (cons 'quote (cons h 'nil)) 'nil))) 'nil))) (cl0 (cons (cons 'hint-please (cons (cons 'quote (cons the-hint 'nil)) 'nil)) (cons (cons 'not (cons (cons 'type-hyp (cons (cons 'hide (cons type-decl-list 'nil)) '(':type))) 'nil)) (cons g/type 'nil)))) (cl1 (cons '(hint-please '(:in-theory (enable type-hyp) :expand ((:free (x) (hide x))))) (cons (cons 'not (cons (cons 'implies (cons (cons 'type-hyp (cons (cons 'hide (cons type-decl-list 'nil)) '(':type))) (cons g/type 'nil))) 'nil)) (cons g 'nil))))) (cons cl0 (cons cl1 'nil)))))
Theorem:
(defthm pseudo-term-list-listp-of-type-extract-fn (b* ((subgoal-lst (type-extract-fn cl smtlink-hint))) (pseudo-term-list-listp subgoal-lst)) :rule-classes :rewrite)
Theorem:
(defthm correctness-of-type-extract-cp (implies (and (pseudo-term-listp cl) (alistp b) (ev-extract (conjoin-clauses (type-extract-fn cl smtlink-hint)) b)) (ev-extract (disjoin cl) b)) :rule-classes :clause-processor)