deftuple

(defun pretty-args
  (hons-opt args)
  (if (atom args)
    nil
    (if hons-opt
      (cons `(hons-list ',(CAR ARGS) ,(CAR ARGS))
        (pretty-args hons-opt (cdr args)))
      (cons `(list ',(CAR ARGS) ,(CAR ARGS))
        (pretty-args hons-opt (cdr args))))))

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

(defun pretty-structurep
  (components x)
  (if (atom components)
    `((eq ,X nil))
    (let ((n (component-name (car components))))
      `((consp ,X) (consp (car ,X))
        (eq (caar ,X) ',N)
        (consp (cdar ,X))
        (eq (cddar ,X) nil)
        ,@(PRETTY-STRUCTUREP (CDR COMPONENTS) `(CDR ,X))))))

(defun deftuple-structure-recognizer
  (name comps guard-opt compact-opt pretty-opt)
  (let* ((ncomps (length comps)) (tests (if pretty-opt
          `((consp x) (eq (car x) ',NAME)
            ,@(PRETTY-STRUCTUREP COMPS '(CDR X)))
          (if compact-opt
            (recog-consp-list ncomps 'x)
            `((true-listp x) (= (length x) ,NCOMPS))))))
    `(defun ,(APPSYMS (LIST NAME 'STRUCTUREP))
      (x)
      ,@(IF GUARD-OPT
      `((DECLARE (XARGS :GUARD T)))
      NIL)
      ,@(IF (< (LEN TESTS) 2)
      TESTS
      `((AND ,@TESTS))))))

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

(defun deftuple-constructor-structure-recognizer-thm
  (name components)
  (let ((call (cons name (components-names components))))
    `(defthm ,(PACKSYMS (LIST NAME '-STRUCTUREP- NAME))
      (,(APPSYMS (LIST NAME 'STRUCTUREP)) ,CALL)
      :rule-classes ((:forward-chaining :trigger-terms (,CALL))))))

(defun deftuple-accessor
  (name component ncomps n guard-opt compact-opt pretty-opt)
  (let ((rec (appsyms (list name 'structurep))) (acc (if pretty-opt
          (if (eq guard-opt :safe)
            `(safe-car (cdr (gentle-assoc ',(COMPONENT-NAME COMPONENT) (safe-cdr x))))
            `(cadr (assoc-eq ',(COMPONENT-NAME COMPONENT) (cdr x))))
          (if compact-opt
            (tree-accessor n ncomps 'x guard-opt)
            (if (eq guard-opt :safe)
              `(safe-nth ,(1- N) x)
              `(nth ,(1- N) x))))))
    `(defun ,(APPSYMS (LIST NAME (COMPONENT-NAME COMPONENT)))
      (x)
      ,@(IF GUARD-OPT
      (IF (EQ GUARD-OPT :SAFE)
          `((DECLARE (XARGS :GUARD T)))
          `((DECLARE (XARGS :GUARD (,REC X)))))
      NIL)
      ,ACC)))

(defun deftuple-accessors-help
  (name components ncomps n guard-opt compact-opt pretty-opt)
  (if (atom components)
    nil
    (cons (deftuple-accessor name
        (car components)
        ncomps
        n
        guard-opt
        compact-opt
        pretty-opt)
      (deftuple-accessors-help name
        (cdr components)
        ncomps
        (1+ n)
        guard-opt
        compact-opt
        pretty-opt))))

(defun deftuple-accessors
  (name components guard-opt compact-opt pretty-opt)
  (deftuple-accessors-help name
    components
    (length components)
    1
    guard-opt
    compact-opt
    pretty-opt))

(defun deftuple-constructor-component-thms
  (name components call)
  (if (atom components)
    nil
    (cons (let* ((arg (component-name (car components))) (acc (appsyms (list name arg))))
        `(defthm ,(APPSYMS (LIST NAME NAME ARG))
          (equal (,ACC ,CALL) ,ARG)))
      (deftuple-constructor-component-thms name
        (cdr components)
        call))))

(defun deftuple-acc-call-list
  (name components)
  (if (atom components)
    nil
    (let* ((cname (component-name (car components))) (acc (appsyms (list name cname))))
      (cons `(,ACC x)
        (deftuple-acc-call-list name (cdr components))))))

(defun deftuple-elim-thm
  (name components)
  (let ((accs (deftuple-acc-call-list name components)))
    `(defthm ,(APPSYMS (LIST NAME 'ELIM))
      (implies (,(APPSYMS (LIST NAME 'STRUCTUREP)) x)
        (equal (,NAME ,@ACCS) x))
      :rule-classes (:rewrite :elim)
      :hints (("Goal" :in-theory (enable true-listp-len-0 nth-open))))))

(defun deftuple-binder
  (name components)
  `(def-patbind-macro ,NAME
    ,(ACCESSOR-LIST (LIST (CONS NAME COMPONENTS)) COMPONENTS)))

(defun accessor-type-list
  (name components)
  (if (atom components)
    nil
    (let ((type (component-type (car components))) (cname (component-name (car components))))
      (if type
        (cons `(,TYPE (,(APPSYMS (LIST NAME CNAME)) x))
          (accessor-type-list name (cdr components)))
        (accessor-type-list name (cdr components))))))

(defun deftuple-recognizer
  (name components guard-opt)
  (let* ((tests (accessor-type-list name components)))
    `(defun ,(PACKSYMS (LIST NAME 'P))
      (x)
      ,@(IF GUARD-OPT
      `((DECLARE (XARGS :GUARD T)))
      NIL)
      (and (,(APPSYMS (LIST NAME 'STRUCTUREP)) x) ,@TESTS))))

(defun deftuple-recognizer-structure-recognizer
  (name)
  `(defthm ,(PACKSYMS (LIST NAME 'P- NAME '-STRUCTUREP))
    (implies (,(PACKSYMS (LIST NAME 'P)) x)
      (,(APPSYMS (LIST NAME 'STRUCTUREP)) x))
    :rule-classes (:rewrite :forward-chaining)))

(defun deftuple-component-type-thms
  (name rec components)
  (if (atom components)
    nil
    (let ((type (component-type (car components))) (acc (appsyms (list name (component-name (car components))))))
      (if type
        (cons `(defthm ,(APPSYMS (LIST REC (COMPONENT-NAME (CAR COMPONENTS))))
            (implies (,REC x) (,TYPE (,ACC x))))
          (deftuple-component-type-thms name rec (cdr components)))
        (deftuple-component-type-thms name rec (cdr components))))))

(defun component-type-list
  (components)
  (if (atom components)
    nil
    (let ((type (component-type (car components))) (name (component-name (car components))))
      (if type
        (cons `(,TYPE ,NAME) (component-type-list (cdr components)))
        (component-type-list (cdr components))))))

(defun deftuple-recognizer-constructor-thm
  (name components)
  (let* ((tests (component-type-list components)) (call `(,NAME ,@(COMPONENTS-NAMES COMPONENTS)))
      (concl `(,(PACKSYMS (LIST NAME 'P)) ,CALL)))
    `(defthm ,(PACKSYMS (LIST NAME 'P- NAME))
      ,(IF (< 0 (LEN TESTS))
     `(EQUAL ,CONCL
             ,@(IF (< 1 (LEN TESTS))
                   `((AND ,@TESTS))
                   TESTS))
     `(EQUAL ,CONCL T)))))

(defun deftuple-defs
  (name components guard-opt hons-opt compact-opt pretty-opt)
  `(,(DEFTUPLE-CONSTRUCTOR NAME COMPONENTS GUARD-OPT HONS-OPT COMPACT-OPT
  PRETTY-OPT) ,(DEFTUPLE-STRUCTURE-RECOGNIZER NAME COMPONENTS GUARD-OPT COMPACT-OPT
  PRETTY-OPT)
    ,(DEFTUPLE-COMPOUND-REC-THM NAME COMPACT-OPT)
    ,(DEFTUPLE-CONSTRUCTOR-STRUCTURE-RECOGNIZER-THM NAME COMPONENTS)
    ,@(DEFTUPLE-ACCESSORS NAME COMPONENTS GUARD-OPT COMPACT-OPT PRETTY-OPT)
    ,@(DEFTUPLE-CONSTRUCTOR-COMPONENT-THMS NAME COMPONENTS
   `(,NAME ,@(COMPONENTS-NAMES COMPONENTS)))
    ,(DEFTUPLE-ELIM-THM NAME COMPONENTS)
    ,(DEFTUPLE-BINDER NAME COMPONENTS)
    ,(DEFTUPLE-RECOGNIZER NAME COMPONENTS GUARD-OPT)
    ,(DEFTUPLE-RECOGNIZER-STRUCTURE-RECOGNIZER NAME)
    ,@(DEFTUPLE-COMPONENT-TYPE-THMS NAME (PACKSYMS (LIST NAME 'P)) COMPONENTS)
    ,(DEFTUPLE-RECOGNIZER-CONSTRUCTOR-THM NAME COMPONENTS)))

(defun deftuple-fn
  (name components kwalist)
  (let* ((guard-opt (kwassoc :guard t kwalist)) (hons-opt (kwassoc :hons nil kwalist))
      (arithmetic-opt (kwassoc :arithmetic t kwalist))
      (pretty-opt (kwassoc :pretty nil kwalist))
      (compact-opt (and (not pretty-opt) (kwassoc :compact nil kwalist)))
      (before-label (appsyms (list 'before name)))
      (difftheory `(set-difference-theories (current-theory :here)
          (current-theory ',BEFORE-LABEL)))
      (function-theory (appsyms (list name 'functions)))
      (exec-theory (appsyms (list name 'executable-counterparts))))
    `(encapsulate nil
      ,@(IF ARITHMETIC-OPT
      `((LOCAL (INCLUDE-BOOK "arithmetic/top-with-meta" :DIR :SYSTEM)))
      NIL)
      (deflabel ,BEFORE-LABEL)
      ,@(DEFTUPLE-DEFS NAME COMPONENTS GUARD-OPT HONS-OPT COMPACT-OPT PRETTY-OPT)
      (deftheory ,FUNCTION-THEORY
        (rules-of-type :definition ,DIFFTHEORY))
      (deftheory ,EXEC-THEORY
        (rules-of-type :executable-counterpart ,DIFFTHEORY))
      (deftheory ,(APPSYMS (LIST NAME 'THEOREMS))
        (set-difference-theories ,DIFFTHEORY
          (union-theories (theory ',FUNCTION-THEORY)
            (theory ',EXEC-THEORY))))
      (in-theory (disable ,FUNCTION-THEORY ,EXEC-THEORY))
      (deftheory ,(APPSYMS (LIST NAME 'ENTIRE-THEORY))
        (set-difference-theories (universal-theory :here)
          (universal-theory ',BEFORE-LABEL))))))

(defun translate-kwalist
  (kwalist)
  (if (atom kwalist)
    nil
    `(cons (cons ',(CAAR KWALIST) ,(CDAR KWALIST))
      ,(TRANSLATE-KWALIST (CDR KWALIST)))))