defsum - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

include-book

(include-book "pattern-match")

include-book

(include-book "types-misc")

other

(set-ignore-ok t)

other

(set-bogus-mutual-recursion-ok t)

product-typefunction

(defun product-type
  (x)
  (declare (xargs :guard (consp x)))
  (car x))

in-theory

(in-theory (disable product-type
    (:executable-counterpart product-type)))

other

(program)

sum-namefunction

(defun sum-name (sum) (car sum))

sum-productsfunction

(defun sum-products (sum) (cdr sum))

sum-recognizerfunction

(defun sum-recognizer
  (sum)
  (appsyms (list (sum-name sum) 'p)))

sym-recognizerfunction

(defun sym-recognizer (sym) (appsyms (list sym 'p)))

product-recognizerfunction

(defun product-recognizer
  (product)
  (or (kwassoc :recognizer nil (product-kwalist product))
    (sym-recognizer (product-name product))))

defsum-munge-productfunction

(defun defsum-munge-product
  (product)
  (mv-let (product kwalist)
    (strip-keywords product)
    (cons (cons (car product) (munge-components (cdr product)))
      kwalist)))

defsum-munge-productsfunction

(defun defsum-munge-products
  (products)
  (if (atom products)
    nil
    (cons (defsum-munge-product (car products))
      (defsum-munge-products (cdr products)))))

strip-extfnsfunction

(defun strip-extfns
  (products)
  (if (atom products)
    (mv nil nil)
    (mv-let (prods extfns)
      (strip-extfns (cdr products))
      (if (and (consp (car products)) (eq (caar products) 'defun))
        (mv prods (cons (car products) extfns))
        (mv (cons (car products) prods) extfns)))))

defsum-munge-inputfunction

(defun defsum-munge-input
  (name rest)
  (mv-let (products kwalist)
    (strip-keywords rest)
    (mv-let (products extfns)
      (strip-extfns products)
      (mv (list (cons name (defsum-munge-products products)))
        extfns
        kwalist))))

defsums-munge-sumsfunction

(defun defsums-munge-sums
  (sums)
  (if (atom sums)
    nil
    (cons (cons (caar sums) (defsum-munge-products (cdar sums)))
      (defsums-munge-sums (cdr sums)))))

defsums-munge-inputfunction

(defun defsums-munge-input
  (args)
  (mv-let (sums kwalist)
    (strip-keywords args)
    (mv-let (sums extfns)
      (strip-extfns sums)
      (mv (defsums-munge-sums sums) extfns kwalist))))

recognizer-namefunction

(defun recognizer-name (sym) (appsyms (list sym 'p)))

recognizer-listfunction

(defun recognizer-list
  (syms)
  (if (atom syms)
    nil
    (cons (recognizer-name (car syms))
      (recognizer-list (cdr syms)))))

constructor-callfunction

(defun constructor-call
  (product)
  (cons (product-name product)
    (components-names (product-components product))))

product-accessor-listfunction

(defun product-accessor-list
  (product)
  (accessor-list product (product-components product)))

accessor-call-listfunction

(defun accessor-call-list
  (product components)
  (if (consp components)
    (cons `(,(ACCESSOR-NAME PRODUCT (CAR COMPONENTS)) x)
      (accessor-call-list product (cdr components)))
    nil))

constructor-deffunction

(defun constructor-def
  (product guard-opt hons-opt compact-opt)
  (let* ((constr (product-name product)) (args (components-names (product-components product)))
      (cons (if hons-opt
          'hons
          'cons)))
    `(defun ,CONSTR
      ,ARGS
      ,@(IF GUARD-OPT
      `((DECLARE (XARGS :GUARD T)))
      NIL)
      ,(IF COMPACT-OPT
     `(,CONS ',CONSTR ,(ARGTREE CONS ARGS))
     `(,(IF HONS-OPT
            'HONS-LIST
            'LIST)
       ',CONSTR ,@ARGS)))))

product-recognizer-deffunction

(defun product-recognizer-def
  (product compact-opt)
  (let* ((nargs (len (product-components product))) (tests (if compact-opt
          (cons `(consp x) (recog-consp-list nargs `(cdr x)))
          `((true-listp x) (= (length x) ,(1+ NARGS))))))
    `(defun ,(PRODUCT-RECOGNIZER PRODUCT)
      (x)
      (declare (xargs :guard t))
      (and ,@TESTS (eq (car x) ',(PRODUCT-NAME PRODUCT))))))

accessor-deffunction

(defun accessor-def
  (product component
    ncomps
    n
    guard-opt
    accessor-opt
    compact-opt)
  (let ((rec (product-recognizer product)) (acc (if compact-opt
          (tree-accessor n ncomps `(cdr x) nil)
          `(nth ,N x))))
    `(defun ,(ACCESSOR-NAME PRODUCT COMPONENT)
      (x)
      ,@(IF GUARD-OPT
      `((DECLARE (XARGS :GUARD (,REC X))))
      NIL)
      ,@(IF (AND GUARD-OPT ACCESSOR-OPT)
      `((MBE :LOGIC (AND (,REC X) ,ACC) :EXEC ,ACC))
      (IF ACCESSOR-OPT
          `((AND (,REC X) ,ACC))
          `(,ACC))))))

accessors-deffunction

(defun accessors-def
  (product components
    ncomps
    n
    guard-opt
    accessor-opt
    compact-opt)
  (if (consp components)
    (cons (accessor-def product
        (car components)
        ncomps
        n
        guard-opt
        accessor-opt
        compact-opt)
      (accessors-def product
        (cdr components)
        ncomps
        (1+ n)
        guard-opt
        accessor-opt
        compact-opt))
    nil))

product-function-defsfunction

(defun product-function-defs
  (product guard-opt hons-opt compact-opt accessor-opt)
  (let* ((kwalist (product-kwalist product)) (predef (kwassoc :predef nil (product-kwalist product)))
      (recog (kwassoc :recognizer nil kwalist)))
    (append (and (not (or recog predef))
        (list (product-recognizer-def product compact-opt)))
      (and (not predef)
        (cons (constructor-def product guard-opt hons-opt compact-opt)
          (accessors-def product
            (product-components product)
            (len (product-components product))
            1
            guard-opt
            accessor-opt
            compact-opt))))))

product-pattern-matcherfunction

(defun product-pattern-matcher
  (product guard-opt)
  `(def-pattern-match-constructor ,(IF (EQ GUARD-OPT :FAST)
     (APPSYMS (LIST (PRODUCT-NAME PRODUCT) 'SLOW))
     (PRODUCT-NAME PRODUCT))
    ,(PRODUCT-RECOGNIZER PRODUCT)
    ,(PRODUCT-ACCESSOR-LIST PRODUCT)))

product-compound-rec-thmfunction

(defun product-compound-rec-thm
  (product compact-opt)
  `(defthm ,(APPSYMS (LIST (PRODUCT-NAME PRODUCT) 'P 'COMPOUND-RECOGNIZER))
    (implies (,(PRODUCT-RECOGNIZER PRODUCT) x)
      ,(IF COMPACT-OPT
     `(CONSP X)
     `(AND (CONSP X) (TRUE-LISTP X))))
    :rule-classes :compound-recognizer))

function-call-listfunction

(defun function-call-list
  (fn-preargs list postargs)
  (if (atom list)
    nil
    (cons (append fn-preargs (cons (car list) postargs))
      (function-call-list fn-preargs (cdr list) postargs))))

args-cons-countfunction

(defun args-cons-count
  (nargs)
  (if (or (zp nargs) (= nargs 1))
    0
    (let ((flo (floor nargs 2)))
      (+ 1 (args-cons-count flo) (args-cons-count (- nargs flo))))))

constructor-acl2-count-thmfunction

(defun constructor-acl2-count-thm
  (product compact-opt)
  (let* ((nargs (len (product-components product))) (conses (if compact-opt
          (1+ (args-cons-count nargs))
          (1+ nargs))))
    `(defthm ,(APPSYMS (LIST (PRODUCT-NAME PRODUCT) 'ACL2-COUNT))
      (equal (acl2-count ,(CONSTRUCTOR-CALL PRODUCT))
        (+ ,CONSES
          ,@(FUNCTION-CALL-LIST '(ACL2-COUNT)
   (COMPONENTS-NAMES (PRODUCT-COMPONENTS PRODUCT)) NIL))))))

accessor-short-circuit-thmfunction

(defun accessor-short-circuit-thm
  (product component)
  (let* ((acc (accessor-name product component)) (rec (product-recognizer product)))
    `(defthm ,(APPSYMS (LIST 'NOT REC ACC))
      (implies (not (,REC x)) (equal (,ACC x) nil)))))

accessor-short-circuit-thmsfunction

(defun accessor-short-circuit-thms
  (product components)
  (if (consp components)
    (cons (accessor-short-circuit-thm product (car components))
      (accessor-short-circuit-thms product (cdr components)))
    nil))

accessor-acl2-count-thmfunction

(defun accessor-acl2-count-thm
  (product component)
  (let ((acc (accessor-name product component)) (recognizer (product-recognizer product)))
    `(defthm ,(APPSYMS (LIST ACC 'ACL2-COUNT))
      (implies (,RECOGNIZER x)
        (< (acl2-count (,ACC x)) (acl2-count x)))
      :hints (("Goal" :in-theory (e/d (acl2-count-car-cdr-of-cons-linear acl2-count-nth-of-len-2-or-greater-linear)
           (nth acl2-count))))
      :rule-classes (:rewrite :linear))))

accessor-acl2-count-thmsfunction

(defun accessor-acl2-count-thms
  (product components)
  (if (consp components)
    (cons (accessor-acl2-count-thm product (car components))
      (accessor-acl2-count-thms product (cdr components)))
    nil))

product-recognizer-constructor-thmfunction

(defun product-recognizer-constructor-thm
  (product)
  (let ((constructor (product-name product)) (constr-call (constructor-call product))
      (recognizer (product-recognizer product)))
    `(defthm ,(APPSYMS (LIST RECOGNIZER CONSTRUCTOR))
      (,RECOGNIZER ,CONSTR-CALL))))

product-elim-thmfunction

(defun product-elim-thm
  (product compact-opt)
  (let ((recognizer (product-recognizer product)) (name (product-name product))
      (components (product-components product)))
    (if (consp components)
      `(defthm ,(APPSYMS (LIST NAME 'ELIM))
        (implies (,RECOGNIZER x)
          (equal (,NAME ,@(ACCESSOR-CALL-LIST PRODUCT COMPONENTS)) x))
        ,@(IF COMPACT-OPT
      NIL
      `(:HINTS (("Goal" :IN-THEORY (ENABLE NTH-OPEN LEN-0-TRUE-LISTP-NOT-X)))))
        :rule-classes (:rewrite :elim))
      `(defthm ,(APPSYMS (LIST NAME 'UNIQUE))
        (implies (,RECOGNIZER x) (equal x (,NAME)))
        :rule-classes :forward-chaining))))

product-type-thmsfunction

(defun product-type-thms
  (product)
  (let ((recognizer (product-recognizer product)) (name (product-name product))
      (call (constructor-call product))
      (components (product-components product)))
    `((defthm ,(APPSYMS (LIST RECOGNIZER 'PRODUCT-TYPE))
       (implies (,RECOGNIZER x) (equal (product-type x) ',NAME))) (defthm ,(APPSYMS (LIST 'PRODUCT-TYPE RECOGNIZER))
        (implies (not (equal (product-type x) ',NAME))
          (not (,RECOGNIZER x))))
      (defthm ,(APPSYMS (LIST NAME 'PRODUCT-TYPE))
        (equal (product-type ,CALL) ',NAME))
      (defthm ,(APPSYMS (LIST NAME 'EQUAL-PRODUCT-TYPE))
        (implies (not (equal (product-type ,CALL) (product-type x)))
          (not (equal ,CALL x)))))))

accessor-constructor-thmfunction

(defun accessor-constructor-thm
  (product component)
  (let ((acc (accessor-name product component)) (constr-call (constructor-call product))
      (arg (component-name component)))
    `(defthm ,(APPSYMS (LIST ACC (PRODUCT-NAME PRODUCT)))
      (equal (,ACC ,CONSTR-CALL) ,ARG))))

constructor-component-thmfunction

(defun constructor-component-thm
  (product component)
  (let ((name (product-name product)) (arg (component-name component)))
    `(defthm ,(APPSYMS (LIST NAME 'NOT-EQUAL ARG))
      (not (equal ,(CONSTRUCTOR-CALL PRODUCT) ,ARG)))))

product-component-thmfunction

(defun product-component-thm
  (product component)
  (let* ((name (product-name product)) (acc (accessor-name product component))
      (recognizer (product-recognizer product)))
    `(defthm ,(APPSYMS (LIST NAME 'NOT-EQUAL ACC))
      (implies (,RECOGNIZER x) (not (equal (,ACC x) x)))
      :hints (("Goal" :use ,(APPSYMS (LIST NAME 'ELIM))
         :in-theory (disable ,NAME ,ACC ,RECOGNIZER))))))

arg-difference-thmfunction

(defun arg-difference-thm
  (product component)
  (let ((arg (component-name component)) (name (product-name product))
      (acc (accessor-name product component)))
    `(defthm ,(APPSYMS (LIST 'DIFFERENCE ARG NAME))
      (implies (not (equal ,ARG (,ACC x)))
        (not (equal ,(CONSTRUCTOR-CALL PRODUCT) x))))))

product-arg-thmsfunction

(defun product-arg-thms
  (product components)
  (if (consp components)
    `(,(ACCESSOR-CONSTRUCTOR-THM PRODUCT (CAR COMPONENTS)) ,(CONSTRUCTOR-COMPONENT-THM PRODUCT (CAR COMPONENTS))
      ,(PRODUCT-COMPONENT-THM PRODUCT (CAR COMPONENTS))
      ,(ARG-DIFFERENCE-THM PRODUCT (CAR COMPONENTS))
      ,@(PRODUCT-ARG-THMS PRODUCT (CDR COMPONENTS)))
    nil))

product-theoremsfunction

(defun product-theorems
  (product accessor-opt compact-opt)
  (let* ((kwalist (product-kwalist product)) (predef (kwassoc :predef nil kwalist))
      (recog (kwassoc :recognizer nil kwalist))
      (components (product-components product)))
    `(,@(AND (NOT PREDEF) (NOT RECOG)
       (LIST (PRODUCT-COMPOUND-REC-THM PRODUCT COMPACT-OPT))) ,@(AND (NOT PREDEF) (LIST (CONSTRUCTOR-ACL2-COUNT-THM PRODUCT COMPACT-OPT)))
      ,@(ACCESSOR-ACL2-COUNT-THMS PRODUCT COMPONENTS)
      ,@(IF ACCESSOR-OPT
      (ACCESSOR-SHORT-CIRCUIT-THMS PRODUCT COMPONENTS)
      NIL)
      ,(PRODUCT-RECOGNIZER-CONSTRUCTOR-THM PRODUCT)
      ,(PRODUCT-ELIM-THM PRODUCT COMPACT-OPT)
      ,@(PRODUCT-ARG-THMS PRODUCT COMPONENTS))))

basic-product-defsfunction

(defun basic-product-defs
  (product guard-opt accessor-opt hons-opt compact-opt)
  (append (product-function-defs product
      guard-opt
      hons-opt
      compact-opt
      accessor-opt)
    (product-theorems product accessor-opt compact-opt)
    (list (product-pattern-matcher product guard-opt))))

defproductmacro

(defmacro defproduct
  (&rest product)
  (let ((product (defsum-munge-product product)))
    `(progn ,@(BASIC-PRODUCT-DEFS PRODUCT (KWASSOC :GUARD NIL (PRODUCT-KWALIST PRODUCT))
   (KWASSOC :SHORT-ACCESSORS T (PRODUCT-KWALIST PRODUCT))
   (KWASSOC :HONS NIL (PRODUCT-KWALIST PRODUCT))
   (KWASSOC :COMPACT T (PRODUCT-KWALIST PRODUCT))))))

basic-products-defsfunction

(defun basic-products-defs
  (products guard-opt accessor-opt hons-opt compact-opt)
  (if (atom products)
    nil
    (append (basic-product-defs (car products)
        guard-opt
        accessor-opt
        hons-opt
        compact-opt)
      (basic-products-defs (cdr products)
        guard-opt
        accessor-opt
        hons-opt
        compact-opt))))

products-type-thmsfunction

(defun products-type-thms
  (products)
  (if (endp products)
    nil
    (append (product-type-thms (car products))
      (products-type-thms (cdr products)))))

type-checklist1function

(defun type-checklist1
  (components)
  (if (consp components)
    (let* ((component (car components)) (type (component-type component))
        (name (component-name component)))
      (if type
        (cons (list type name) (type-checklist1 (cdr components)))
        (type-checklist1 (cdr components))))
    nil))

type-checklistfunction

(defun type-checklist
  (components)
  (let ((checklist (type-checklist1 components)))
    (if checklist
      (if (consp (cdr checklist))
        `(and ,@CHECKLIST)
        (car checklist))
      t)))

sum-recognizer-clausefunction

(defun sum-recognizer-clause
  (product guard-opt)
  (let* ((type-checklist (type-checklist (product-components product))) (constr (constructor-call product))
      (pattern (if (eq guard-opt :fast)
          (cons (appsyms (list (car constr) 'slow)) (cdr constr))
          constr)))
    (list pattern type-checklist)))

sum-recognizer-clausesfunction

(defun sum-recognizer-clauses
  (products guard-opt)
  (if (consp products)
    (cons (sum-recognizer-clause (car products) guard-opt)
      (sum-recognizer-clauses (cdr products) guard-opt))
    nil))

sum-recognizer-deffunction

(defun sum-recognizer-def
  (sum guard-opt)
  `(defun ,(SUM-RECOGNIZER SUM)
    (x)
    (declare (xargs :measure (1+ (acl2-count x))
        ,@(IF GUARD-OPT
      `(:GUARD T)
      NIL)
        :hints (("goal" :in-theory (enable acl2-count-nth-of-len-2-or-greater-linear)))))
    (pattern-match x
      ,@(SUM-RECOGNIZER-CLAUSES (SUM-PRODUCTS SUM) GUARD-OPT))))

sum-recognizer-defsfunction

(defun sum-recognizer-defs
  (sums guard-opt)
  (if (consp sums)
    (cons (sum-recognizer-def (car sums) guard-opt)
      (sum-recognizer-defs (cdr sums) guard-opt))
    nil))

sum-recognizers-deffunction

(defun sum-recognizers-def
  (sums extfns guard-opt)
  (if (and (= (len sums) 1) (not extfns))
    (sum-recognizer-def (car sums) guard-opt)
    `(mutual-recursion ,@(SUM-RECOGNIZER-DEFS SUMS GUARD-OPT)
      ,@EXTFNS)))

sum-compound-rec-thmfunction

(defun sum-compound-rec-thm
  (sum compact-opt)
  (let ((sumname (sum-name sum)) (recognizer (sum-recognizer sum)))
    `(defthm ,(APPSYMS (LIST SUMNAME 'COMPOUND-RECOGNIZER))
      (implies (,RECOGNIZER x)
        ,(IF COMPACT-OPT
     `(CONSP X)
     `(AND (CONSP X) (TRUE-LISTP X))))
      :rule-classes :compound-recognizer)))

sum-compound-rec-thmsfunction

(defun sum-compound-rec-thms
  (sums compact-opt)
  (if (consp sums)
    (cons (sum-compound-rec-thm (car sums) compact-opt)
      (sum-compound-rec-thms (cdr sums) compact-opt))
    nil))

recognizer-call-listfunction

(defun recognizer-call-list
  (products)
  (if (consp products)
    (cons `(,(PRODUCT-RECOGNIZER (CAR PRODUCTS)) x)
      (recognizer-call-list (cdr products)))
    nil))

sum-possibility-thmfunction

(defun sum-possibility-thm
  (sum)
  (let ((rec-list (recognizer-call-list (sum-products sum))) (name (sum-name sum))
      (recognizer (sum-recognizer sum)))
    `(defthm ,(APPSYMS (LIST NAME 'POSSIBILITIES))
      (implies (,RECOGNIZER x)
        ,(IF (CONSP (CDR REC-LIST))
     `(OR ,@REC-LIST)
     (CAR REC-LIST)))
      :rule-classes :forward-chaining)))

sum-possibility-thmsfunction

(defun sum-possibility-thms
  (sums)
  (if (consp sums)
    (cons (sum-possibility-thm (car sums))
      (sum-possibility-thms (cdr sums)))
    nil))

product-fast-recsfunction

(defun product-fast-recs
  (products sumrec)
  (if (atom products)
    nil
    (let* ((product (car products)) (pname (product-name product))
        (prec (product-recognizer product))
        (prfast (appsyms (list prec 'fast))))
      (append `((defun ,PRFAST
           (x)
           (declare (xargs :guard (,SUMREC x)))
           (mbe :exec (eq (car x) ',PNAME) :logic (,PREC x))) (def-pattern-match-constructor ,PNAME
            ,PRFAST
            ,(PRODUCT-ACCESSOR-LIST PRODUCT)))
        (product-fast-recs (cdr products) sumrec)))))

product-fast-recs-sumsfunction

(defun product-fast-recs-sums
  (sums)
  (if (atom sums)
    nil
    (append (product-fast-recs (sum-products (car sums))
        (sum-recognizer (car sums)))
      (product-fast-recs-sums (cdr sums)))))

accessor-type-checklist1function

(defun accessor-type-checklist1
  (product components)
  (if (consp components)
    (let ((ctype (component-type (car components))) (prodname (product-name product))
        (acc (accessor-name product (car components))))
      (if ctype
        (cons `(,CTYPE (,ACC x))
          (accessor-type-checklist1 product (cdr components)))
        (accessor-type-checklist1 product (cdr components))))
    nil))

accessor-type-checklistfunction

(defun accessor-type-checklist
  (product)
  (let ((checklist (accessor-type-checklist1 product
         (product-components product))))
    (if (consp checklist)
      (if (consp (cdr checklist))
        `(and ,@CHECKLIST)
        (car checklist))
      t)))

strip-product-recognizersfunction

(defun strip-product-recognizers
  (products)
  (if (atom products)
    nil
    (cons (product-recognizer (car products))
      (strip-product-recognizers (cdr products)))))

accessor-type-thmfunction

(defun accessor-type-thm
  (sum product)
  (let ((checklist (accessor-type-checklist product)) (prodname (product-name product))
      (srecog (sum-recognizer sum))
      (sumname (sum-name sum))
      (recogs (strip-product-recognizers (sum-products sum)))
      (precog (product-recognizer product)))
    (if (eq checklist t)
      nil
      `((defthm ,(APPSYMS (LIST SUMNAME PRODNAME 'ACCESSOR-TYPES))
         (implies (and (,SRECOG x) (,PRECOG x)) ,CHECKLIST)
         :hints (("Goal" :in-theory (disable ,@RECOGS
              ,PRODNAME
              ,@(PRODUCT-ACCESSOR-LIST PRODUCT))
            :expand ((,SRECOG x)))))))))

accessor-type-thmsfunction

(defun accessor-type-thms
  (sum products)
  (if (consp products)
    (append (accessor-type-thm sum (car products))
      (accessor-type-thms sum (cdr products)))
    nil))

all-accessor-type-thmsfunction

(defun all-accessor-type-thms
  (sums)
  (if (consp sums)
    (append (accessor-type-thms (car sums) (sum-products (car sums)))
      (all-accessor-type-thms (cdr sums)))
    nil))

negated-listfunction

(defun negated-list
  (list)
  (if (atom list)
    nil
    (cons (list 'not (car list)) (negated-list (cdr list)))))

negated-accessor-type-listfunction

(defun negated-accessor-type-list
  (product)
  (let ((nlist (negated-list (accessor-type-checklist1 product
           (product-components product)))))
    (if (atom nlist)
      nil
      (if (atom (cdr nlist))
        (car nlist)
        `(or ,@NLIST)))))

bad-typing-thmfunction

(defun bad-typing-thm
  (sum product)
  (let ((badtypes (negated-accessor-type-list product)) (srecog (sum-recognizer sum))
      (precog (product-recognizer product))
      (sumname (sum-name sum))
      (pname (product-name product)))
    (if badtypes
      `((defthm ,(APPSYMS (LIST PNAME 'NOT SUMNAME))
         (implies (and (,PRECOG x) ,BADTYPES) (not (,SRECOG x)))
         :hints (("Goal" :in-theory (disable ,PRECOG ,@(PRODUCT-ACCESSOR-LIST PRODUCT))))))
      nil)))

sum-bad-typing-thmsfunction

(defun sum-bad-typing-thms
  (sum products)
  (if (consp products)
    (append (bad-typing-thm sum (car products))
      (sum-bad-typing-thms sum (cdr products)))
    nil))

all-bad-typing-thmsfunction

(defun all-bad-typing-thms
  (sums)
  (if (consp sums)
    (append (sum-bad-typing-thms (car sums) (sum-products (car sums)))
      (all-bad-typing-thms (cdr sums)))
    nil))

sum-recognizer-constructor-thmfunction

(defun sum-recognizer-constructor-thm
  (sum product)
  (let ((constructor (product-name product)) (precog (product-recognizer product))
      (constr-call (constructor-call product))
      (recognizer (sum-recognizer sum))
      (type-checklist (type-checklist (product-components product))))
    `(defthm ,(APPSYMS (LIST RECOGNIZER CONSTRUCTOR))
      ,(IF (EQ T TYPE-CHECKLIST)
     `(,RECOGNIZER ,CONSTR-CALL)
     `(IFF (,RECOGNIZER ,CONSTR-CALL) ,TYPE-CHECKLIST))
      :hints (("Goal" :in-theory (disable ,PRECOG
           ,CONSTRUCTOR
           ,@(PRODUCT-ACCESSOR-LIST PRODUCT)))))))

sum-recognizer-constructor-thmsfunction

(defun sum-recognizer-constructor-thms
  (sum products)
  (if (consp products)
    `(,(SUM-RECOGNIZER-CONSTRUCTOR-THM SUM (CAR PRODUCTS)) ,@(SUM-RECOGNIZER-CONSTRUCTOR-THMS SUM (CDR PRODUCTS)))
    nil))

all-post-constructor-thmsfunction

(defun all-post-constructor-thms
  (sums)
  (if (consp sums)
    (append (sum-recognizer-constructor-thms (car sums)
        (sum-products (car sums)))
      (all-post-constructor-thms (cdr sums)))
    nil))

recognizer-negate-listfunction

(defun recognizer-negate-list
  (products arg)
  (if (consp products)
    (cons `(not (,(PRODUCT-RECOGNIZER (CAR PRODUCTS)) ,ARG))
      (recognizer-negate-list (cdr products) arg))
    nil))

not-equal-constructor-listfunction

(defun not-equal-constructor-list
  (term products)
  (if (consp products)
    (cons `(not (equal ,TERM ,(CONSTRUCTOR-CALL (CAR PRODUCTS))))
      (not-equal-constructor-list term (cdr products)))
    nil))

exclusion-thmfunction

(defun exclusion-thm
  (product all-products)
  (let* ((rest (remove-equal product all-products)) (not-prod (recognizer-negate-list rest (constructor-call product)))
      (not-equal (not-equal-constructor-list (constructor-call product) rest))
      (not-recs (recognizer-negate-list rest 'x))
      (name (product-name product))
      (recognizer (product-recognizer product)))
    (if not-prod
      `((defthm ,(APPSYMS (LIST NAME 'NOT-OTHERS))
         ,(IF (= (LEN NOT-PROD) 1)
     (CAR NOT-PROD)
     `(AND ,@NOT-PROD))
         :hints (("Goal" :in-theory (disable true-listp len)))) (defthm ,(APPSYMS (LIST NAME 'NOT-OTHER-CONSTRUCTORS))
          ,(IF (= (LEN NOT-EQUAL) 1)
     (CAR NOT-EQUAL)
     `(AND ,@NOT-EQUAL)))
        (defthm ,(APPSYMS (LIST RECOGNIZER 'NOT-OTHERS))
          (implies (,RECOGNIZER x)
            ,(IF (= (LEN NOT-RECS) 1)
     (CAR NOT-RECS)
     `(AND ,@NOT-RECS)))
          :hints (("Goal" :in-theory (disable true-listp len)))
          :rule-classes :forward-chaining))
      nil)))

exclusion-thmsfunction

(defun exclusion-thms
  (products all-products)
  (if (consp products)
    (append (exclusion-thm (car products) all-products)
      (exclusion-thms (cdr products) all-products))
    nil))

name-matching-recognizerfunction

(defun name-matching-recognizer
  (sums predtyp)
  (if (atom sums)
    nil
    (if (eq predtyp (sum-recognizer (car sums)))
      (sum-name (car sums))
      (name-matching-recognizer (cdr sums) predtyp))))

recursive-arg-and-call-listfunction

(defun recursive-arg-and-call-list
  (sums components)
  (if (consp components)
    (let ((predtyp (component-type (car components))))
      (mv-let (args calls)
        (recursive-arg-and-call-list sums (cdr components))
        (if predtyp
          (let ((typname (name-matching-recognizer sums predtyp)) (argname (component-name (car components))))
            (if typname
              (mv (cons argname args)
                (cons `(,(APPSYMS (LIST TYPNAME 'MEASURE)) ,ARGNAME) calls))
              (mv (cons '& args) calls)))
          (mv (cons '& args) calls))))
    (mv nil nil)))

measure-clause-listfunction

(defun measure-clause-list
  (sums products)
  (if (consp products)
    (let ((rest (measure-clause-list sums (cdr products))))
      (mv-let (args calls)
        (recursive-arg-and-call-list sums
          (product-components (car products)))
        (if (consp calls)
          (cons `((,(PRODUCT-NAME (CAR PRODUCTS)) ,@ARGS) (+ 1 ,@CALLS))
            rest)
          rest)))
    '((& 1))))

measure-deffunction

(defun measure-def
  (sum sums guard-opt)
  (let ((clauses (measure-clause-list sums (sum-products sum))))
    `(defun ,(APPSYMS (LIST (SUM-NAME SUM) 'MEASURE))
      (x)
      (declare (xargs :measure (acl2-count x)
          ,@(CASE GUARD-OPT
    (:FAST `(:GUARD (,(SUM-RECOGNIZER SUM) X)))
    (() NIL)
    (OTHERWISE `(:GUARD T))))
        ,@(IF (= (LEN CLAUSES) 1)
      `((IGNORE X))
      NIL))
      (pattern-match x ,@CLAUSES))))

measure-defsfunction

(defun measure-defs
  (sums all-sums guard-opt)
  (if (consp sums)
    (cons (measure-def (car sums) all-sums guard-opt)
      (measure-defs (cdr sums) all-sums guard-opt))
    nil))

measure-mrecfunction

(defun measure-mrec
  (sums guard-opt)
  (let ((mdefs (measure-defs sums sums guard-opt)))
    (if (= (len mdefs) 1)
      (car mdefs)
      `(mutual-recursion ,@MDEFS))))

field-measure-ineqsfunction

(defun field-measure-ineqs
  (sums measure prodname prodargs)
  (if (consp prodargs)
    (let* ((predtyp (component-type (car prodargs))) (arg (component-name (car prodargs)))
        (pred (name-matching-recognizer sums predtyp))
        (meas (appsyms (list pred 'measure)))
        (acc (appsyms (list prodname arg))))
      (if pred
        (cons `(< (,MEAS (,ACC x)) (,MEASURE x))
          (field-measure-ineqs sums measure prodname (cdr prodargs)))
        (field-measure-ineqs sums measure prodname (cdr prodargs))))
    nil))

field-measure-thmsfunction

(defun field-measure-thms
  (sums measure products)
  (if (consp products)
    (let ((ineqs (field-measure-ineqs sums
           measure
           (product-name (car products))
           (product-components (car products)))))
      (if ineqs
        (cons `(defthm ,(APPSYMS (LIST (PRODUCT-NAME (CAR PRODUCTS)) 'MEASURE-DECR))
            (implies (,(PRODUCT-RECOGNIZER (CAR PRODUCTS)) x)
              ,(IF (CONSP (CDR INEQS))
     `(AND ,@INEQS)
     (CAR INEQS))))
          (field-measure-thms sums measure (cdr products)))
        (field-measure-thms sums measure (cdr products))))
    nil))

sum-measure-thmsfunction

(defun sum-measure-thms
  (sums all-sums)
  (if (consp sums)
    (append (field-measure-thms all-sums
        (appsyms (list (sum-name (car sums)) 'measure))
        (sum-products (car sums)))
      (sum-measure-thms (cdr sums) all-sums))
    nil))

updater-defunfunction

(defun updater-defun
  (prodname args accs n guard-opt)
  (let ((name (nth (1- n) args)))
    `(defun ,(APPSYMS (LIST 'UPDATE PRODNAME NAME))
      (new x)
      ,@(IF GUARD-OPT
      `((DECLARE
         (XARGS :GUARD (,(RECOGNIZER-NAME PRODNAME) X) :GUARD-HINTS
          (("Goal" :IN-THEORY (ENABLE ,PRODNAME))))))
      NIL)
      (mbe :exec (update-nth ,N new x)
        :logic (,PRODNAME ,@(UPDATE-NTH (1- N) 'NEW ACCS))))))

product-updater-defunsfunction

(defun product-updater-defuns
  (prodname args accs n guard-opt)
  (if (zp n)
    nil
    (cons (updater-defun prodname args accs n guard-opt)
      (product-updater-defuns prodname args accs (1- n) guard-opt))))

updater-defunsfunction

(defun updater-defuns
  (products guard-opt)
  (if (atom products)
    nil
    (let* ((prodname (product-name (car products))) (components (product-components (car products)))
        (arglist (components-names components)))
      (append (product-updater-defuns prodname
          arglist
          (accessor-call-list (car products) components)
          (len arglist)
          guard-opt)
        (updater-defuns (cdr products) guard-opt)))))

sums-productsfunction

(defun sums-products
  (sums)
  (if (atom sums)
    nil
    (append (sum-products (car sums))
      (sums-products (cdr sums)))))

sums-namesfunction

(defun sums-names
  (sums)
  (if (atom sums)
    nil
    (cons (sum-name (car sums)) (sums-names (cdr sums)))))

defsums-fnfunction

(defun defsums-fn
  (sums kwalist extfns)
  (let* ((products (sums-products sums)) (guard-option (kwassoc :guard t kwalist))
      (hons-opt (kwassoc :hons nil kwalist))
      (compact-opt (kwassoc :compact t kwalist))
      (accessor-option (kwassoc :short-accessors t kwalist))
      (update-option (kwassoc :updatable nil kwalist))
      (arith-option (kwassoc :arithmetic t kwalist))
      (theory-name (appsyms (sums-names sums)))
      (before-label (appsyms (list 'before theory-name))))
    `(encapsulate nil
      (set-bogus-measure-ok t)
      (deflabel ,BEFORE-LABEL)
      (local (in-theory (enable product-type (:executable-counterpart product-type))))
      ,@(IF ARITH-OPTION
      `((LOCAL (INCLUDE-BOOK "arithmetic/top-with-meta" :DIR :SYSTEM)))
      NIL)
      ,@(BASIC-PRODUCTS-DEFS PRODUCTS GUARD-OPTION ACCESSOR-OPTION HONS-OPT
   COMPACT-OPT)
      ,(SUM-RECOGNIZERS-DEF SUMS EXTFNS GUARD-OPTION)
      ,@(SUM-COMPOUND-REC-THMS SUMS COMPACT-OPT)
      ,@(SUM-POSSIBILITY-THMS SUMS)
      ,@(EXCLUSION-THMS PRODUCTS PRODUCTS)
      ,@(ALL-ACCESSOR-TYPE-THMS SUMS)
      ,@(ALL-BAD-TYPING-THMS SUMS)
      ,@(ALL-POST-CONSTRUCTOR-THMS SUMS)
      (deftheory ,(APPSYMS (LIST THEORY-NAME 'FUNCTIONS))
        (rules-of-type :definition (set-difference-theories (current-theory :here)
            (current-theory ',BEFORE-LABEL))))
      ,@(IF (EQ GUARD-OPTION :FAST)
      (PRODUCT-FAST-RECS-SUMS SUMS)
      NIL)
      (deftheory ,(APPSYMS (LIST THEORY-NAME 'EXECUTABLE-COUNTERPARTS))
        (rules-of-type :executable-counterpart (set-difference-theories (current-theory :here)
            (current-theory ',BEFORE-LABEL))))
      (deftheory ,(APPSYMS (LIST THEORY-NAME 'INDUCTIONS))
        (rules-of-type :induction (set-difference-theories (current-theory :here)
            (current-theory ',BEFORE-LABEL))))
      (deftheory ,(APPSYMS (LIST THEORY-NAME 'THEOREMS))
        (set-difference-theories (set-difference-theories (current-theory :here)
            (current-theory ',BEFORE-LABEL))
          (union-theories (theory ',(APPSYMS (LIST THEORY-NAME 'EXECUTABLE-COUNTERPARTS)))
            (union-theories (theory ',(APPSYMS (LIST THEORY-NAME 'FUNCTIONS)))
              (theory ',(APPSYMS (LIST THEORY-NAME 'INDUCTIONS)))))))
      ,@(PRODUCTS-TYPE-THMS PRODUCTS)
      (deftheory ,(APPSYMS (LIST THEORY-NAME 'PRODUCT-TYPE-THEOREMS))
        (set-difference-theories (current-theory :here)
          (current-theory ',(APPSYMS (LIST THEORY-NAME 'THEOREMS)))))
      (in-theory (disable ,(APPSYMS (LIST THEORY-NAME 'FUNCTIONS))
          ,(APPSYMS (LIST THEORY-NAME 'EXECUTABLE-COUNTERPARTS))
          ,(APPSYMS (LIST THEORY-NAME 'PRODUCT-TYPE-THEOREMS))))
      ,@(AND (NOT EXTFNS)
       `(,(MEASURE-MREC SUMS GUARD-OPTION) ,@(SUM-MEASURE-THMS SUMS SUMS)))
      ,@(IF UPDATE-OPTION
      (UPDATER-DEFUNS PRODUCTS GUARD-OPTION)
      NIL)
      (deftheory ,(APPSYMS (LIST THEORY-NAME 'ENTIRE-THEORY))
        (set-difference-theories (universal-theory :here)
          (universal-theory ',BEFORE-LABEL))))))

other

(defxdoc defsum
  :parents (miscellaneous)
  :short "Define a recursive data type similar to a Haskell type definition."
  :long "<p>Example:</p>

 @({
 (include-book "tools/defsum" :dir :system)
 (set-ignore-ok :warn)
 (defsum my-list
   (my-empty)
   (my-cons car (my-list-p cdr)))
 })

<p>This declaration says that an object is of the type @('my-list') if it
is either of the type @('my-empty') or @('my-cons'), where @('my-empty')
is an empty structure and @('my-cons') is a structure with two fields:
the @('car'), an arbitrary object; and the @('cdr') which is of type
@('my-list').  In this case, recognizers @('my-list-p'), @('my-empty-p'),
and @('my-cons-p') are defined along with constructors @('my-empty') and
@('my-cons') and destructors @('my-cons-car') and @('my-cons-cdr').  The
necessary macros are also defined to enable pattern-matching using the
constructors (see @(see pattern-match)).  For mutually-recursive data types
see @(see defsums).  It may also be informative to look at the translated
version of a defsum form using :trans1.</p>

<p>Note that a defsum form produces several logic-mode events inside an
encapsulate.  Despite the author's best intentions, not every such
automatically-generated event will complete successfully.  If you
encounter a defsum form that fails, please email it to
sswords@cs.utexas.edu (with or without fixing the bug yourself.)</p>

<p>Several theorems about the new type are defined so as to enable
reasoning based on their abstract model rather than their underlying
list representation. For most reasoning these theorems should be
sufficient without enabling the function definitions or
executable-counterparts.  In case these do need to be enabled,
theories named (for the above example) @('my-list-functions') and
@('my-list-executable-counterparts') are defined.</p>

<p>In addition to the recognizer, constructor, and destructor functions,
a measure function is also defined which counts the number of nested
objects of the sum type.  In the example above, the measure function
is my-list-measure and the measure of an object is 1 if it is not a
my-cons, and 1 plus the measure of its my-cons-cdr if it is.</p>

<p>Defsum accepts some keyword arguments.  Be aware that not all
combinations of these arguments have been tested extensively.  Again,
please send bug reports to sswords@cs.utexas.edu if you find a defsum
form that does not succeed.</p>

<p>@(':arithmetic') - By default, each @('defsum') event expands to an
encapsulate which locally includes the book arithmetic/top-with-meta.
If an incompatible arithmetic book has already been included, this may
cause the defsum to fail.  But the other arithmetic book may also have
theorems that allow the defsum event to succeed if we don't attempt to
include the arithmetic book.  This can be done by setting
@(':arithmetic nil').</p>

<p>@(':guard') - may be set to @('t'), @('nil'), or @(':fast').  By default
it is set to @('t'), in which case minimal guards are set for all
functions.  If set to @('nil'), guards will not be verified for any
functions; this is useful in case some field type recognizers don't
have their guards verified.  If set to @(':fast'), an additional
recognizer for each product is defined named ``foo-p-fast'' if the
product is named foo.  This has a guard such that its argument must be
a valid sum object.  It is then logically equivalent to the other
recognizer, but in execution only checks that the symbol in the car of
the object matches the name of the product.  The pattern matcher for
each product then uses the fast recognizers.  Thus fast guards result
in a small (?) gain in performance in exchange for a (hopefully
trivial) degradation in logical complexity.</p>

<p>@(':short-accessors') - @('t') by default; may be set to @('nil').  If
@('t'), each field accessor first checks whether the object is of the
correct product type and returns nil if not.  This allows for an
additional theorem saying that if x is not of the correct product
type, then the accessor returns nil.  If @('nil'), the nth accessor
returns @('(nth n x)') regardless of x's type.  When guards are turned
on, this is implemented with an @('mbe') so there should be no
performance difference between the two options.  When guards are off,
performance will be somewhat better if this feature is turned off.</p>

<p>@(':compact') - By default, a defsum constructor makes a product
object by putting its components into a cons tree using n-1 conses,
but a prettier list representation is also supported which uses n
conses to store the elements in a flattened list which is easier to
read when printed.  Set @(':compact nil') if you prefer this
representation.</p>

<p>@(':hons') - If HONS mode is in use, the flag @(':hons t') causes all
defsum forms to be built with HONSes rather than regular conses.  See
@(see hons-and-memoization).</p>

<p>It may be necessary to include some function definition in a mutual
recursion with the sum recognizer function.  In this case simply put
the defun form inside the defsum form, i.e.</p>

 @({
 (defsum lisp-term
   (lisp-atom val)
   (func-app (symbolp function) (lisp-term-listp args))
   (defun lisp-term-listp (args)
     (declare (xargs :guard t))
     (if (atom args)
         (null args)
       (and (lisp-term-p (car args))
            (lisp-term-listp (cdr args))))))
 })

<p>If such a function is included, however, no measure function will be
defined for the sum.</p>

<p>Usually it is not necessary to specify a measure for such a function;
because there is currently no way of directly specifying the measure
for the sum's recognizer, specifying an exotic measure on such a
function is likely to fail.  If you come up against this limitation,
please send an example to sswords@cs.utexas.edu.</p>")

defsummacro

(defmacro defsum
  (name &rest defs)
  (mv-let (sum extfns kwalist)
    (defsum-munge-input name defs)
    (defsums-fn sum kwalist extfns)))

other

(defxdoc defsums
  :parents (miscellaneous)
  :short "Define a set of mutually-recursive data types."
  :long "<p>Example:</p>

 @({
 (defsums
   (my-term
    (my-atom val)
    (my-application (symbolp function) (my-term-list-p args)))
   (my-term-list
    (my-nil)
    (my-cons (my-term-p car) (my-term-list-p cdr))))
 })

<p>See @(see defsum).  This form is used when you want to define two or more
types which may be constructed from each other.  In the above example,
@('my-term') and @('my-term-list') could not be defined using independent
defsum forms; their recognizer functions need to be defined in a mutual
recursion.</p>

<p>Defsums accepts the same keyword arguments as defsum.</p>

<p>If you want some function to be defined inside the same mutual-recursion in
which the recognizers for each of the sums and products are defined, you may
insert the defun inside the def-mutual-sums form, i.e.</p>

 @({
 (defsums
  (foo
   (bla (bar-p x))
   (ble (foo-p x) (bar-p y)))
  (bar
   (blu (integerp k))
   (blo (symbolp f) (foo-list-p a)))
  (defun foo-list-p (x)
    (declare (xargs :guard t))
    (if (atom x)
        (null x)
      (and (foo-p (car x))
           (foo-list-p (cdr x))))))
 })

<p>Usually it is not necessary to specify a measure for such a function;
because there is currently no way of directly specifying the measures on the
sums' recognizers, specifying an exotic measure on such a function is likely to
fail.</p>

<p>As with defsum, def-mutual-sums requires the (possibly local) inclusion of
the defsum-thms book.</p>")

defsumsmacro

(defmacro defsums
  (&rest sums)
  (mv-let (sums extfns kwalist)
    (defsums-munge-input sums)
    (defsums-fn sums kwalist extfns)))