decomp-hint - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "join-thms")

include-book

(include-book "std/util/bstar" :dir :system)

find-expands-for-arg-termmutual-recursion

(mutual-recursion (defun find-expands-for-arg-term
    (x arg world def-alist exclude)
    (b* (((when (atom x)) (mv nil nil)) ((when (eq (car x) 'quote)) (mv nil nil))
        ((mv expands found) (find-expands-for-arg-list (cdr x)
            arg
            world
            def-alist
            exclude))
        ((when expands) (mv expands found))
        ((unless (or found (member-equal arg (cdr x)))) (mv nil nil))
        ((when (or (member (car x) exclude)
             (consp (car x))
             (member (car x) '(not car cdr)))) (mv nil nil))
        (look (assoc (car x) def-alist))
        ((when look) (mv `((:with ,(CDR LOOK) ,X)) nil))
        ((when (fgetprop (car x) 'def-bodies nil world)) (mv (list x) nil)))
      (mv nil t)))
  (defun find-expands-for-arg-list
    (x arg world def-alist exclude)
    (if (atom x)
      (mv nil nil)
      (b* (((mv car-ex car-f) (find-expands-for-arg-term (car x)
             arg
             world
             def-alist
             exclude)) ((mv cdr-ex cdr-f) (find-expands-for-arg-list (cdr x)
              arg
              world
              def-alist
              exclude)))
        (mv (union-equal car-ex cdr-ex) (or car-f cdr-f))))))

find-expands-for-arg-clausefunction

(defun find-expands-for-arg-clause
  (x arg world def-alist exclude)
  (mv-let (expands found)
    (find-expands-for-arg-list x arg world def-alist exclude)
    (declare (ignore found))
    expands))

present-in-termmutual-recursion

(mutual-recursion (defun present-in-term
    (x subt)
    (cond ((equal x subt) t)
      ((atom x) nil)
      ((eq (car x) 'quote) nil)
      (t (present-in-term-list (cdr x) subt))))
  (defun present-in-term-list
    (x subt)
    (and (consp x)
      (or (present-in-term (car x) subt)
        (present-in-term-list (cdr x) subt)))))

structure-decomposefunction

(defun structure-decompose (x) (declare (ignore x)) t)

in-theory

(in-theory (disable structure-decompose
    (structure-decompose)
    (:type-prescription structure-decompose)))

other

(defevaluator strdec-ev
  strdec-ev-lst
  ((if x
     y
     z) (structure-decompose x)
    (not x)))

other

(def-join-thms strdec-ev)

consed-subtermsfunction

(defun consed-subterms
  (term)
  (case-match term
    (('cons a b . &) (union-equal (consed-subterms a) (consed-subterms b)))
    (& (list term))))

consed-subterm-present-in-termfunction

(defun consed-subterm-present-in-term
  (term consed)
  (if (atom consed)
    nil
    (or (present-in-term term (car consed))
      (consed-subterm-present-in-term term (cdr consed)))))

remove-terms-without-presentfunction

(defun remove-terms-without-present
  (clause subterms)
  (if (atom clause)
    clause
    (let ((rest (remove-terms-without-present (cdr clause) subterms)))
      (if (consed-subterm-present-in-term (car clause) subterms)
        (if (equal rest (cdr clause))
          clause
          (cons (car clause) rest))
        rest))))

strdec-ev-remove-terms-without-presenttheorem

(defthm strdec-ev-remove-terms-without-present
  (implies (strdec-ev (disjoin (remove-terms-without-present clause struct))
      alist)
    (strdec-ev (disjoin clause) alist)))

select-expand-substructfunction

(defun select-expand-substruct
  (clause substruct)
  (list (cons `(not (structure-decompose ,SUBSTRUCT))
      (remove-terms-without-present clause
        (consed-subterms substruct)))))

remove-irrel-cpfunction

(defun remove-irrel-cp
  (clause substruct)
  (list (remove-terms-without-present clause
      (consed-subterms substruct))))

select-expand-substruct-correcttheorem

(defthm select-expand-substruct-correct
  (implies (and (pseudo-term-listp clause)
      (alistp a)
      (strdec-ev (conjoin-clauses (select-expand-substruct clause substruct))
        a))
    (strdec-ev (disjoin clause) a))
  :hints (("goal" :in-theory (e/d (structure-decompose)
       (consed-subterms consed-subterm-present-in-term))))
  :rule-classes :clause-processor)

remove-irrel-cp-correcttheorem

(defthm remove-irrel-cp-correct
  (implies (and (pseudo-term-listp clause)
      (alistp a)
      (strdec-ev (conjoin-clauses (remove-irrel-cp clause substruct))
        a))
    (strdec-ev (disjoin clause) a))
  :hints (("goal" :in-theory (e/d (structure-decompose)
       (consed-subterms consed-subterm-present-in-term))))
  :rule-classes :clause-processor)

structural-decomp-hint-carefulfunction

(defun structural-decomp-hint-careful
  (clause arg stablep state def-alist exclude)
  (declare (xargs :stobjs state :mode :program))
  (b* (((unless stablep) (value nil)) (world (w state))
      ((er arg) (translate arg
          t
          nil
          nil
          'structural-decomp-hint-careful
          world
          state))
      (expands (find-expands-for-arg-clause clause
          arg
          world
          def-alist
          exclude))
      ((when expands) (value `(:computed-hint-replacement ((structural-decomp-hint-careful clause
               ',ARG
               stable-under-simplificationp
               state
               ',DEF-ALIST
               ',EXCLUDE))
            :expand ,EXPANDS)))
      (car `(car ,ARG))
      (cdr `(cdr ,ARG))
      (concl (car (last clause)))
      ((mv 1st 2nd give-up) (cond ((present-in-term concl car) (mv car cdr nil))
          ((present-in-term concl cdr) (mv cdr car nil))
          ((present-in-term-list clause car) (mv car cdr nil))
          ((present-in-term-list clause cdr) (mv cdr car nil))
          (t (mv car cdr t)))))
    (if give-up
      (prog2$ (cw "Giving up on structural expansion~%")
        (value '(:no-op t)))
      (value `(:computed-hint-replacement ((after-select-substruct-hint clause
             stable-under-simplificationp
             state
             ',DEF-ALIST
             ',EXCLUDE))
          :or ((:clause-processor (select-expand-substruct clause ',1ST)) (:clause-processor (select-expand-substruct clause ',2ND))
            (:no-op t)))))))

after-select-substruct-hintfunction

(defun after-select-substruct-hint
  (clause stablep state def-alist exclude)
  (declare (xargs :stobjs state :mode :program))
  (let ((term (car clause)))
    (case-match term
      (('not ('structure-decompose arg)) (structural-decomp-hint-careful clause
          arg
          stablep
          state
          def-alist
          exclude))
      (& (prog2$ (cw "After-select-substruct-hint didn't find the
chosen structure to decompose. Clause: ~x0~%"
            clause)
          (value '(:no-op t)))))))

structural-decomp-hint-fastfunction

(defun structural-decomp-hint-fast
  (clause arg stablep state def-alist exclude)
  (declare (xargs :stobjs state :mode :program))
  (b* (((unless stablep) (value nil)) (world (w state))
      ((er arg) (translate arg
          t
          nil
          nil
          'structural-decomp-hint-fast
          world
          state))
      (expands (find-expands-for-arg-clause clause
          arg
          world
          def-alist
          exclude))
      ((when expands) (value `(:computed-hint-replacement ((structural-decomp-hint-fast clause
               ',ARG
               stable-under-simplificationp
               state
               ',DEF-ALIST
               ',EXCLUDE))
            :expand ,EXPANDS)))
      (car (if (and (consp arg) (eq (car arg) 'cons))
          (cadr arg)
          `(car ,ARG)))
      (cdr (if (and (consp arg) (eq (car arg) 'cons))
          (caddr arg)
          `(cdr ,ARG)))
      (concl (car (last clause)))
      ((mv 1st give-up) (cond ((present-in-term concl car) (mv car nil))
          ((present-in-term concl cdr) (mv cdr nil))
          ((present-in-term-list clause car) (mv car nil))
          ((present-in-term-list clause cdr) (mv cdr nil))
          (t (mv car t)))))
    (if give-up
      (prog2$ (cw "Giving up on structural expansion~%")
        (value '(:no-op t)))
      (value `(:computed-hint-replacement ((structural-decomp-hint-fast clause
             ',1ST
             stable-under-simplificationp
             state
             ',DEF-ALIST
             ',EXCLUDE))
          :clause-processor (remove-irrel-cp clause ',1ST))))))

structural-decompmacro

(defmacro structural-decomp
  (arg &key do-not-expand def-alist)
  `(structural-decomp-hint-fast clause
    ',ARG
    stable-under-simplificationp
    state
    (append ',DEF-ALIST
      (table-alist 'structural-decomp-defs (w state)))
    ,DO-NOT-EXPAND))

structural-decomp-carefulmacro

(defmacro structural-decomp-careful
  (arg &key do-not-expand def-alist)
  `(structural-decomp-hint-careful clause
    ',ARG
    stable-under-simplificationp
    state
    (append ',DEF-ALIST
      (table-alist 'structural-decomp-defs (w state)))
    ,DO-NOT-EXPAND))