		Search-engine friendly clone of the ACL2 documentation.

Smt-extract

Extract

Functions for extracting type declarations from clause.

Definitions and Theorems

Function: extract-disjunct

(defun extract-disjunct (term fty-info abs)
 (declare (xargs :guard (and (pseudo-termp term)
                             (fty-info-alist-p fty-info)
                             (symbol-listp abs))))
 (let ((acl2::__function__ 'extract-disjunct))
  (declare (ignorable acl2::__function__))
  (b* ((term (pseudo-term-fix term)))
   (cond
     ((not (consp term)) (mv nil term))
     ((and (equal (car term) 'if)
           (equal (caddr term) ''t))
      (b* (((mv decl1 term1)
            (extract-disjunct (cadr term)
                              fty-info abs))
           ((mv decl2 term2)
            (extract-disjunct (cadddr term)
                              fty-info abs)))
        (mv (append decl1 decl2)
            (cond ((or (equal term1 ''t) (equal term2 ''t))
                   ''t)
                  ((equal term1 ''nil) term2)
                  ((equal term2 ''nil) term1)
                  (t (cons 'if
                           (cons term1
                                 (cons ''t (cons term2 'nil)))))))))
     ((equal (car term) 'not)
      (b* (((mv decl0 term0)
            (extract-conjunct (cadr term)
                              fty-info abs)))
        (mv decl0
            (cond ((equal term0 ''nil) ''t)
                  ((equal term0 ''t) ''nil)
                  (t (cons 'not (cons term0 'nil)))))))
     ((equal (car term) 'implies)
      (b* (((mv decl1 term1)
            (extract-conjunct (cadr term)
                              fty-info abs))
           ((mv decl2 term2)
            (extract-disjunct (caddr term)
                              fty-info abs)))
        (mv (append decl1 decl2)
            (cond ((or (equal term1 ''nil)
                       (equal term2 ''t))
                   ''t)
                  ((equal term1 ''t) term2)
                  ((equal term2 ''nil)
                   (cons 'not (cons term1 'nil)))
                  (t (cons 'implies
                           (cons term1 (cons term2 'nil))))))))
     (t (mv nil term))))))

Function: extract-conjunct

(defun extract-conjunct (term fty-info abs)
 (declare (xargs :guard (and (pseudo-termp term)
                             (fty-info-alist-p fty-info)
                             (symbol-listp abs))))
 (let ((acl2::__function__ 'extract-conjunct))
  (declare (ignorable acl2::__function__))
  (b* ((term (pseudo-term-fix term)))
   (cond
       ((not (consp term)) (mv nil term))
       ((and (equal (car term) 'if)
             (equal (cadddr term) ''nil))
        (b* (((mv decl1 term1)
              (extract-conjunct (cadr term)
                                fty-info abs))
             ((mv decl2 term2)
              (extract-conjunct (caddr term)
                                fty-info abs)))
          (mv (append decl1 decl2)
              (cond ((or (equal term1 ''nil)
                         (equal term2 ''nil))
                     ''nil)
                    ((equal term1 ''t) term2)
                    ((equal term2 ''t) term1)
                    (t (cons 'if
                             (cons term1 (cons term2 '('nil)))))))))
       ((equal (car term) 'not)
        (b* (((mv decl0 term0)
              (extract-disjunct (cadr term)
                                fty-info abs)))
          (mv decl0
              (cond ((equal term0 ''nil) ''t)
                    ((equal term0 ''t) ''nil)
                    (t (cons 'not (cons term0 'nil)))))))
       ((extract-is-decl term fty-info abs)
        (mv (list term) ''t))
       (t (mv nil term))))))

Theorem: return-type-of-extract-disjunct.decl-list

(defthm return-type-of-extract-disjunct.decl-list
  (b* (((mv ?decl-list ?theorem)
        (extract-disjunct term fty-info abs)))
    (pseudo-term-listp decl-list))
  :rule-classes :rewrite)

Theorem: return-type-of-extract-disjunct.theorem

(defthm return-type-of-extract-disjunct.theorem
  (b* (((mv ?decl-list ?theorem)
        (extract-disjunct term fty-info abs)))
    (pseudo-termp theorem))
  :rule-classes :rewrite)

Theorem: return-type-of-extract-conjunct.decl-list

(defthm return-type-of-extract-conjunct.decl-list
  (b* (((mv ?decl-list ?theorem)
        (extract-conjunct term fty-info abs)))
    (pseudo-term-listp decl-list))
  :rule-classes :rewrite)

Theorem: return-type-of-extract-conjunct.theorem

(defthm return-type-of-extract-conjunct.theorem
  (b* (((mv ?decl-list ?theorem)
        (extract-conjunct term fty-info abs)))
    (pseudo-termp theorem))
  :rule-classes :rewrite)

Subtopics

Extract-disjunct
Extract-conjunct