fty-sum-casemacro

(defun kind-casemacro-casespec-p
  (spec)
  (and (consp spec)
    (symbolp (car spec))
    (consp (cdr spec))
    (if (atom (cadr spec))
      (and (symbolp (cadr spec)) (not (cddr spec)))
      (and (consp (cadr spec))
        (symbol-listp (cadr spec))
        (consp (cddr spec))
        (symbolp (caddr spec))
        (not (cdddr spec))))))

(defun kind-casemacro-casespecs-p
  (specs)
  (if (atom specs)
    (eq specs nil)
    (and (kind-casemacro-casespec-p (car specs))
      (kind-casemacro-casespecs-p (cdr specs)))))

(defun kind-casemacro-spec-p
  (spec)
  (and (consp spec)
    (symbolp (car spec))
    (consp (cdr spec))
    (symbolp (cadr spec))
    (kind-casemacro-casespecs-p (cddr spec))))

(defun kind-casemacro-cases
  (var cases kwd-alist)
  (declare (xargs :guard (kind-casemacro-casespecs-p cases)))
  (b* (((when (atom kwd-alist)) nil) ((when (or (eq (caar kwd-alist) :otherwise)
           (eq (caar kwd-alist) :otherwise*))) `((otherwise ,(CDAR FTY::KWD-ALIST))))
      (kind (caar kwd-alist))
      (case-spec (cdr (assoc kind cases)))
      (subkindsp (consp (car case-spec)))
      (ctor (if subkindsp
          (cadr case-spec)
          (car case-spec))))
    (cons `(,(COND ((ATOM (CDR FTY::KWD-ALIST)) 'OTHERWISE)
       (FTY::SUBKINDSP (CAR FTY::CASE-SPEC)) (T FTY::KIND)) (b* (((,FTY::CTOR ,FTY::VAR :quietp t)))
          ,(CDAR FTY::KWD-ALIST)))
      (kind-casemacro-cases var
        cases
        (cdr kwd-alist)))))

(defun kind-casemacro-prod-kinds
  (cases)
  (declare (xargs :guard (kind-casemacro-casespecs-p cases)))
  (if (atom cases)
    nil
    (if (consp (cadar cases))
      (append (cadar cases)
        (kind-casemacro-prod-kinds (cdr cases)))
      (cons (caar cases)
        (kind-casemacro-prod-kinds (cdr cases))))))

(defun kind-casemacro-check-prod-kinds-covered
  (cases keys seen)
  (declare (xargs :guard (kind-casemacro-casespecs-p cases)))
  (b* (((when (atom keys)) (let ((diff (set-difference-eq (kind-casemacro-prod-kinds cases)
              seen)))
         (and diff
           (er hard?
             'kind-casemacro-fn
             "No case covers product kinds ~x0~%"
             (remove-duplicates-eq diff))))) (kind (car keys))
      ((when (or (eq kind :otherwise) (eq kind :otherwise*))) (let ((diff (set-difference-eq (kind-casemacro-prod-kinds cases)
               seen)))
          (and (not diff)
            (if (eq kind :otherwise)
              (er hard?
                'kind-casemacro-fn
                "Redundant :otherwise entry.~%")
              t))))
      (case-spec (cdr (assoc kind cases)))
      (prods (if (consp (car case-spec))
          (car case-spec)
          (list kind)))
      ((when (subsetp prods seen)) (er hard?
          'kind-casemacro-fn
          "Redundant case: ~x0~%"
          kind)))
    (kind-casemacro-check-prod-kinds-covered cases
      (cdr keys)
      (append prods seen))))

(defun kind-casemacro-fn
  (var-or-expr rest-args case-spec)
  (b* (((unless (kind-casemacro-spec-p case-spec)) (er hard?
         'kind-casemacro-fn
         "Bad case-spec: ~x0~%"
         case-spec)) ((list* macro-name kind-fn case-specs) case-spec)
      (case-kinds (remove-duplicates-eq (strip-cars case-specs)))
      (prod-kinds (remove-duplicates-eq (kind-casemacro-prod-kinds case-specs)))
      ((when (and (eql (len rest-args) 1)
           (or (atom (car rest-args))
             (eq (caar rest-args) 'quote)))) (cond ((and (atom (car rest-args))
             (member-eq (car rest-args) prod-kinds)) `(eq (,FTY::KIND-FN ,FTY::VAR-OR-EXPR) ,(CAR FTY::REST-ARGS)))
          ((and (atom (car rest-args))
             (member-eq (car rest-args) case-kinds)) `(member-eq (,FTY::KIND-FN ,FTY::VAR-OR-EXPR)
              ',(CADR (ASSOC (CAR FTY::REST-ARGS) FTY::CASE-SPECS))))
          ((and (eq (caar rest-args) 'quote)
             (true-listp (cadr rest-args))
             (subsetp (cadr rest-args) prod-kinds)) `(member-eq (,FTY::KIND-FN ,FTY::VAR-OR-EXPR)
              ,(CAR FTY::REST-ARGS)))
          (t (cond ((equal case-kinds prod-kinds) (er hard?
                  macro-name
                  "Bad argument: ~x0~% Must be one of ~x1 or a quoted subset.~%"
                  (car rest-args)
                  case-kinds))
              (t (er hard?
                  macro-name
                  "Bad argument: ~x0~% Must be one of ~x1 or a quoted subset of ~x2.~%"
                  (car rest-args)
                  (union-eq prod-kinds case-kinds)
                  prod-kinds))))))
      ((when (consp var-or-expr)) (er hard?
          macro-name
          "Expected a variable, rather than: ~x0"
          var-or-expr))
      (var var-or-expr)
      (allowed-keywordlist-keys (append case-kinds '(:otherwise :otherwise*)))
      (allowed-parenthesized-keys (append case-kinds
          '(otherwise :otherwise :otherwise* &)))
      ((mv kwd-alist rest) (extract-keywords macro-name
          allowed-keywordlist-keys
          rest-args
          nil))
      ((when (and rest kwd-alist)) (er hard?
          macro-name
          "Inconsistent syntax: ~x0"
          rest-args))
      ((unless (or kwd-alist
           (and (alistp rest)
             (true-list-listp rest)
             (subsetp (strip-cars rest)
               allowed-parenthesized-keys)))) (er hard?
          macro-name
          "Malformed cases: ~x0~%"
          rest))
      (kwd-alist (reverse kwd-alist))
      (keys (if kwd-alist
          (strip-cars kwd-alist)
          (sublis '((otherwise . :otherwise) (& . :otherwise))
            (strip-cars rest))))
      (vals (if kwd-alist
          (strip-cdrs kwd-alist)
          (pairlis$ (make-list (len rest) :initial-element 'progn$)
            (strip-cdrs rest))))
      ((unless (and (<= (len (member :otherwise keys)) 1)
           (<= (len (member :otherwise* keys)) 1))) (er hard?
          macro-name
          "Otherwise case must be last"))
      (redundant-otherwise* (kind-casemacro-check-prod-kinds-covered case-specs
          keys
          nil))
      (kind-kwd-alist (or kwd-alist (pairlis$ keys vals)))
      (kind-kwd-alist (if redundant-otherwise*
          (remove-assoc-eq :otherwise* kind-kwd-alist)
          kind-kwd-alist))
      (body (if (eq (caar kind-kwd-alist) :otherwise*)
          (cdar kind-kwd-alist)
          (let ((var.kind (intern-in-package-of-symbol (concatenate 'string (symbol-name var) ".KIND")
                 (if (equal (symbol-package-name var) "COMMON-LISP")
                   'acl2
                   var))))
            `(let* ((,FTY::VAR.KIND (,FTY::KIND-FN ,FTY::VAR)))
              (declare (ignorable ,FTY::VAR.KIND))
              (case ,FTY::VAR.KIND . ,(FTY::KIND-CASEMACRO-CASES FTY::VAR FTY::CASE-SPECS FTY::KIND-KWD-ALIST)))))))
    body))

(defun cond-casemacro-casespec-p
  (spec)
  (and (consp spec)
    (symbolp (car spec))
    (consp (cdr spec))
    (consp (cddr spec))
    (symbolp (caddr spec))
    (not (cdddr spec))))

(defun cond-casemacro-casespecs-p
  (specs)
  (if (atom specs)
    (eq specs nil)
    (and (cond-casemacro-casespec-p (car specs))
      (cond-casemacro-casespecs-p (cdr specs)))))

(defun cond-casemacro-spec-p
  (spec)
  (and (consp spec)
    (symbolp (car spec))
    (consp (cdr spec))
    (symbolp (cadr spec))
    (cond-casemacro-casespecs-p (cddr spec))))

(defun cond-casemacro-cases
  (var cond-var cases kwd-alist)
  (declare (xargs :guard (cond-casemacro-casespecs-p cases)))
  (b* (((when (atom cases)) nil) ((list kwd cond-expr ctor) (car cases))
      (entry (cdr (assoc kwd kwd-alist)))
      (test (if (and (atom (cdr cases)) (eq cond-expr t))
          t
          `(let ((,FTY::COND-VAR ,FTY::VAR))
            ,FTY::COND-EXPR))))
    (cons `(,FTY::TEST (b* (((,FTY::CTOR ,FTY::VAR :quietp t))) ,FTY::ENTRY))
      (cond-casemacro-cases var
        cond-var
        (cdr cases)
        kwd-alist))))

(defun cond-casemacro-list-conditions
  (kwds kinds)
  (if (atom kinds)
    nil
    `(,(CAR FTY::KINDS) ,(IF (MEMBER (CAR FTY::KINDS) FTY::KWDS)
     T
     NIL) . ,(FTY::COND-CASEMACRO-LIST-CONDITIONS FTY::KWDS (CDR FTY::KINDS)))))

(defun cond-casemacro-fn
  (var-or-expr rest-args case-spec)
  (b* (((unless (cond-casemacro-spec-p case-spec)) (er hard?
         'cond-casemacro-fn
         "Bad case-spec: ~x0~%"
         case-spec)) ((list* macro-name cond-var case-specs) case-spec)
      (case-kinds (remove-duplicates-eq (strip-cars case-specs)))
      ((when (and (eql (len rest-args) 1)
           (or (atom (car rest-args))
             (eq (caar rest-args) 'quote)))) (b* (((mv var binding) (if (symbolp var-or-expr)
               (mv var-or-expr nil)
               (mv cond-var
                 `((,FTY::COND-VAR ,FTY::VAR-OR-EXPR))))) (caselist (if (atom (car rest-args))
                (list (car rest-args))
                (cadr (car rest-args))))
            ((unless (subsetp-eq caselist case-kinds)) (er hard?
                macro-name
                "Bad argument: ~x0~% Must be one of ~x1 or a quoted subset.~%"
                (car rest-args)
                case-kinds))
            (new-args (cond-casemacro-list-conditions caselist
                case-kinds))
            (body (cond-casemacro-fn var
                new-args
                case-spec)))
          (if binding
            `(b* ,FTY::BINDING ,FTY::BODY)
            body)))
      ((when (consp var-or-expr)) (er hard?
          macro-name
          "Expected a variable, rather than: ~x0"
          var-or-expr))
      (var var-or-expr)
      (allowed-keywordlist-keys (append case-kinds '(:otherwise)))
      (allowed-parenthesized-keys (append case-kinds '(otherwise :otherwise &)))
      ((mv kwd-alist rest) (extract-keywords macro-name
          allowed-keywordlist-keys
          rest-args
          nil))
      ((when (and rest kwd-alist)) (er hard?
          macro-name
          "Inconsistent syntax: ~x0"
          rest-args))
      ((unless (or kwd-alist
           (and (alistp rest)
             (true-list-listp rest)
             (subsetp (strip-cars rest)
               allowed-parenthesized-keys)))) (er hard?
          macro-name
          "Malformed cases: ~x0~%"
          rest))
      (kwd-alist (reverse kwd-alist))
      (keys (if kwd-alist
          (strip-cars kwd-alist)
          (sublis '((otherwise . :otherwise) (& . :otherwise))
            (strip-cars rest))))
      (vals (if kwd-alist
          (strip-cdrs kwd-alist)
          (pairlis$ (make-list (len rest) :initial-element 'progn$)
            (strip-cdrs rest))))
      ((unless (<= (len (member :otherwise keys)) 1)) (er hard?
          macro-name
          "Otherwise case must be last"))
      (kind-kwd-alist (or kwd-alist (pairlis$ keys vals)))
      (body `(cond . ,(FTY::COND-CASEMACRO-CASES FTY::VAR FTY::COND-VAR FTY::CASE-SPECS
  FTY::KIND-KWD-ALIST))))
    body))