defagg - ACL2 Book

other

(in-package "GL")

other

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

other

(include-book "tools/flag" :dir :system)

other

(include-book "tools/pattern-match" :dir :system)

other

(logic)

other

(defund-inline tag
  (x)
  (declare (xargs :guard (consp x)))
  (car x))

other

(defthm tag-of-cons
  (equal (tag (cons a b)) a)
  :hints (("Goal" :in-theory (enable tag))))

other

(defthm tag-forward-to-cons
  (implies (tag x) (consp x))
  :hints (("Goal" :in-theory (enable tag)))
  :rule-classes :forward-chaining)

other

(defthm tag-when-atom
  (implies (not (consp x))
    (equal (tag x) nil))
  :hints (("Goal" :in-theory (enable tag)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

other

(program)

list-to-tree-aux1function

(defun list-to-tree-aux1
  (depth lst)
  (declare (xargs :guard (and (natp depth) (consp lst))))
  (cond ((atom (cdr lst)) (mv (car lst) nil))
    ((zp depth) (mv (car lst) (cdr lst)))
    (t (b* (((mv first rest) (list-to-tree-aux1 (1- depth) lst)) ((when (atom rest)) (mv first rest))
          ((mv snd rest) (list-to-tree-aux1 (1- depth) rest)))
        (mv (cons first snd) rest)))))

other

(defthm list-to-tree-aux1-decr
  (implies (consp lst)
    (< (len (mv-nth 1 (list-to-tree-aux1 depth lst)))
      (len lst)))
  :rule-classes :linear)

list-to-tree-auxfunction

(defun list-to-tree-aux
  (depth fst lst)
  (declare (xargs :guard (natp depth)
      :measure (len lst)))
  (b* (((when (atom lst)) fst) ((mv snd rest) (list-to-tree-aux1 depth lst))
      (tree1 (cons fst snd))
      ((when (atom rest)) tree1))
    (list-to-tree-aux (1+ depth) tree1 rest)))

list-to-treefunction

(defun list-to-tree
  (lst)
  (declare (xargs :guard t))
  (if (atom lst)
    nil
    (list-to-tree-aux 0 (car lst) (cdr lst))))

alist-wrap-pairsfunction

(defun alist-wrap-pairs
  (car/cdr alist)
  (declare (xargs :guard (alistp alist)))
  (if (atom alist)
    nil
    (cons (cons (caar alist)
        `(and (consp x)
          (let* ((x (,GL::CAR/CDR (the cons x))))
            ,(CDAR GL::ALIST))))
      (alist-wrap-pairs car/cdr (cdr alist)))))

mk-accs-alistfunction

(defun mk-accs-alist
  (basename tree)
  (declare (xargs :guard t))
  (if (atom tree)
    (list (cons (da-accessor-name basename tree) 'x))
    (append (alist-wrap-pairs 'car
        (mk-accs-alist basename (car tree)))
      (alist-wrap-pairs 'cdr
        (mk-accs-alist basename (cdr tree))))))

mk-accessorsfunction

(defun mk-accessors
  (accs-alist tag)
  (if (atom accs-alist)
    nil
    (cons `(defund-inline ,(CAAR GL::ACCS-ALIST)
        (x)
        (declare (xargs :guard (and . ,(AND GL::TAG `((CONSP GL::X) (EQ (GL::TAG GL::X) ',GL::TAG))))))
        ,(IF GL::TAG
     `(LET* ((GL::X (CDR (THE CONS GL::X))))
        ,(CDAR GL::ACCS-ALIST))
     (CDAR GL::ACCS-ALIST)))
      (mk-accessors (cdr accs-alist) tag))))

mk-constructor-auxfunction

(defun mk-constructor-aux
  (tree)
  (if (atom tree)
    tree
    `(cons ,(GL::MK-CONSTRUCTOR-AUX (CAR GL::TREE))
      ,(GL::MK-CONSTRUCTOR-AUX (CDR GL::TREE)))))

mk-constructorfunction

(defun mk-constructor
  (basename tag names tree notinline)
  `(,(IF NOTINLINE
     'GL::DEFUND
     'GL::DEFUND-INLINE) ,GL::BASENAME
    ,GL::NAMES
    (declare (xargs :guard t))
    ,(IF GL::TAG
     `(CONS ',GL::TAG ,(GL::MK-CONSTRUCTOR-AUX GL::TREE))
     (GL::MK-CONSTRUCTOR-AUX GL::TREE))))

accessors-of-constructorfunction

(defun accessors-of-constructor
  (basename accs-alist fields all-fields)
  (if (atom fields)
    nil
    (let ((acc (caar accs-alist)))
      (cons `(defthm ,(GL::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME GL::ACC) "-OF-" (SYMBOL-NAME GL::BASENAME))
  GL::BASENAME)
          (equal (,GL::ACC (,GL::BASENAME . ,GL::ALL-FIELDS))
            ,(CAR GL::FIELDS))
          :hints (("Goal" :in-theory (enable ,GL::ACC ,GL::BASENAME))))
        (accessors-of-constructor basename
          (cdr accs-alist)
          (cdr fields)
          all-fields)))))

accessor-acl2-count-thmsfunction

(defun accessor-acl2-count-thms
  (basename accs-alist)
  (if (atom accs-alist)
    nil
    (let ((acc (caar accs-alist)))
      (cons `(defthm ,(GL::INTERN-IN-PACKAGE-OF-SYMBOL
  (CONCATENATE 'STRING (SYMBOL-NAME GL::ACC) "-ACL2-COUNT-THM") GL::BASENAME)
          (implies (consp x)
            (< (acl2-count (,GL::ACC x)) (acl2-count x)))
          :hints (("Goal" :in-theory (enable ,GL::ACC)))
          :rule-classes (:rewrite :linear))
        (accessor-acl2-count-thms basename
          (cdr accs-alist))))))

defagg-fnfunction

(defun defagg-fn
  (basename fields tag notinline)
  (b* ((tree (list-to-tree fields)) (accs-alist (mk-accs-alist basename tree))
      (?accs (strip-cars accs-alist)))
    `(defsection ,GL::BASENAME
      ,(GL::MK-CONSTRUCTOR GL::BASENAME GL::TAG GL::FIELDS GL::TREE NOTINLINE)
      ,@(GL::MK-ACCESSORS GL::ACCS-ALIST GL::TAG)
      ,@(GL::ACCESSORS-OF-CONSTRUCTOR GL::BASENAME GL::ACCS-ALIST GL::FIELDS
   GL::FIELDS)
      ,@(GL::ACCESSOR-ACL2-COUNT-THMS GL::BASENAME GL::ACCS-ALIST)
      ,@(AND GL::TAG
       `((GL::DEFTHM
          ,(GL::INTERN-IN-PACKAGE-OF-SYMBOL
            (CONCATENATE 'STRING "TAG-OF-" (SYMBOL-NAME GL::BASENAME))
            GL::BASENAME)
          (EQUAL (GL::TAG (,GL::BASENAME . ,GL::FIELDS)) ',GL::TAG) :HINTS
          (("Goal" :IN-THEORY (GL::ENABLE ,GL::BASENAME GL::TAG))))
         (DEFMACRO ,(GL::INTERN-IN-PACKAGE-OF-SYMBOL
                     (CONCATENATE 'STRING (SYMBOL-NAME GL::BASENAME) "-P")
                     GL::BASENAME)
                   (GL::X)
           `(EQ (GL::TAG ,GL::X) ',',GL::TAG))
         (GL::DEF-PATTERN-MATCH-CONSTRUCTOR (GL::X) ,GL::BASENAME
          (EQ (GL::TAG GL::X) ',GL::TAG) ,GL::ACCS))))))

defaggmacro

(defmacro defagg
  (basename fields
    &key
    (tag 'nil tag-p)
    notinline)
  (defagg-fn basename
    fields
    (if tag-p
      tag
      (intern (symbol-name basename) "KEYWORD"))
    notinline))

other

(logic)

other

(local (defagg foo (a b) :tag :foo))