multicase - ACL2 Book

other

(in-package "FTY")

other

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

other

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

other

(program)

multicase-case-decompfunction

(defun multicase-case-decomp
  (case)
  (case-match case
    ((match ':when cond val) (mv match cond val))
    ((match ':when cond val) (mv match cond val))
    ((match val) (mv match t val))
    (& (prog2$ (er hard?
          'multicase
          "Illformed case: ~x0"
          case)
        (mv nil nil nil)))))

multicase-wildcard-pfunction

(defun multicase-wildcard-p
  (x)
  (or (eq x ':otherwise)
    (and (symbolp x)
      (or (equal (symbol-name x) "&")
        (equal (symbol-name x) "-")))))

multicase-empty-cases-assemblefunction

(defun multicase-empty-cases-assemble
  (cases)
  (b* (((when (atom cases)) nil) ((mv match cond val) (multicase-case-decomp (car cases)))
      ((when (and match
           (not (multicase-wildcard-p match)))) (er hard? 'multicase "Extra match fields"))
      ((when (eq cond t)) val))
    `(if ,COND
      ,FTY::VAL
      ,(FTY::MULTICASE-EMPTY-CASES-ASSEMBLE (CDR FTY::CASES)))))

multicase-matches-decompfunction

(defun multicase-matches-decomp
  (match)
  (if (multicase-wildcard-p match)
    (mv :otherwise :otherwise)
    (mv (if (multicase-wildcard-p (car match))
        :otherwise (car match))
      (cdr match))))

cases-collect-leading-keysfunction

(defun cases-collect-leading-keys
  (cases)
  (b* (((when (atom cases)) nil) (rest (cases-collect-leading-keys (cdr cases)))
      ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first &) (multicase-matches-decomp match))
      ((when (member-equal first rest)) rest))
    (cons first rest)))

case-change-matchfunction

(defun case-change-match
  (match case)
  (cons match (cdr case)))

filter-wildcard-casesfunction

(defun filter-wildcard-cases
  (cases)
  (b* (((when (atom cases)) nil) ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first rest) (multicase-matches-decomp match))
      ((when (multicase-wildcard-p first)) (cons (case-change-match rest (car cases))
          (filter-wildcard-cases (cdr cases)))))
    (filter-wildcard-cases (cdr cases))))

filter-key-casesfunction

(defun filter-key-cases
  (key cases)
  (b* (((when (atom cases)) nil) ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first rest) (multicase-matches-decomp match))
      ((when (or (multicase-wildcard-p first)
           (equal first key))) (cons (case-change-match rest (car cases))
          (filter-key-cases key (cdr cases)))))
    (filter-key-cases key (cdr cases))))

list-has-consp-casesfunction

(defun list-has-consp-cases
  (cases)
  (b* (((when (atom cases)) nil) ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first &) (multicase-matches-decomp match))
      ((when (atom first)) (list-has-consp-cases (cdr cases))))
    t))

list-has-endp-casesfunction

(defun list-has-endp-cases
  (cases)
  (b* (((when (atom cases)) nil) ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first &) (multicase-matches-decomp match))
      ((when (eq first nil)) t))
    (list-has-endp-cases (cdr cases))))

list-process-consp-casesfunction

(defun list-process-consp-cases
  (cases)
  (b* (((when (atom cases)) nil) ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first rest) (multicase-matches-decomp match))
      ((when (multicase-wildcard-p first)) (cons (case-change-match (list* first first rest)
            (car cases))
          (list-process-consp-cases (cdr cases))))
      ((when (atom first)) (list-process-consp-cases (cdr cases)))
      ((cons first-first rest-first) first))
    (cons (case-change-match (list* first-first rest-first rest)
        (car cases))
      (list-process-consp-cases (cdr cases)))))

list-process-wildcard-casesfunction

(defun list-process-wildcard-cases
  (cases)
  (b* (((when (atom cases)) nil) ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first rest) (multicase-matches-decomp match))
      ((when (multicase-wildcard-p first)) (cons (case-change-match rest (car cases))
          (list-process-wildcard-cases (cdr cases)))))
    (list-process-wildcard-cases (cdr cases))))

list-process-endp-casesfunction

(defun list-process-endp-cases
  (cases)
  (b* (((when (atom cases)) nil) ((mv match & &) (multicase-case-decomp (car cases)))
      ((mv first rest) (multicase-matches-decomp match))
      ((unless (or (multicase-wildcard-p first) (eq first nil))) (list-process-endp-cases (cdr cases))))
    (cons (case-change-match rest (car cases))
      (list-process-endp-cases (cdr cases)))))

other

(mutual-recursion (defun multicase-fn
    (pairs cases)
    (b* (((when (atom pairs)) (multicase-empty-cases-assemble cases)) ((list casemacro var) (car pairs))
        ((mv listp casemacro vars) (case-match casemacro
            (('list mac . vars) (mv t mac vars))
            (& (if (atom casemacro)
                (mv nil casemacro nil)
                (prog2$ (er hard? 'multicase-fn "bad casemacro")
                  (mv nil nil nil))))))
        ((when listp) (b* ((has-cons (list-has-consp-cases cases)) (has-end (list-has-endp-cases cases))
              (end-cases (list-process-endp-cases cases))
              (check-consp (or has-cons has-end)))
            (if check-consp
              `(if (consp ,FTY::VAR)
                ,(IF FTY::HAS-CONS
     (FTY::B* ((FTY::CONS-CASES (FTY::LIST-PROCESS-CONSP-CASES FTY::CASES)))
      `(LET* ((,(CAR FTY::VARS) (CAR ,FTY::VAR))
              (FTY::MULTICASE-TMP (CDR ,FTY::VAR)))
         (DECLARE (IGNORABLE FTY::MULTICASE-TMP ,(CAR FTY::VARS)))
         ,(FTY::MULTICASE-FN
           (LIST* `(,FTY::CASEMACRO ,(CAR FTY::VARS))
                  `((LIST ,FTY::CASEMACRO . ,(CDR FTY::VARS))
                    FTY::MULTICASE-TMP)
                  (CDR FTY::PAIRS))
           FTY::CONS-CASES)))
     (FTY::B* ((FTY::WILD-CASES (FTY::LIST-PROCESS-WILDCARD-CASES FTY::CASES)))
      (FTY::MULTICASE-FN (CDR FTY::PAIRS) FTY::WILD-CASES)))
                ,(FTY::MULTICASE-FN (CDR FTY::PAIRS) FTY::END-CASES))
              (multicase-fn (cdr pairs) end-cases))))
        (match-keys (cases-collect-leading-keys cases))
        (has-wildcard (member-eq :otherwise match-keys))
        (non-wildcard-keys (remove-eq :otherwise match-keys)))
      `(,FTY::CASEMACRO ,FTY::VAR . ,(FTY::MULTICASE-COLLECT-SUBCASES FTY::NON-WILDCARD-KEYS FTY::HAS-WILDCARD
  (CDR FTY::PAIRS) FTY::CASES))))
  (defun multicase-collect-subcases
    (keys has-wildcard pairs cases)
    (if (atom keys)
      (and has-wildcard
        `(:otherwise* ,(FTY::MULTICASE-FN FTY::PAIRS (FTY::FILTER-WILDCARD-CASES FTY::CASES))))
      (b* ((key (car keys)))
        `(,FTY::KEY ,(FTY::MULTICASE-FN FTY::PAIRS (FTY::FILTER-KEY-CASES FTY::KEY FTY::CASES)) . ,(FTY::MULTICASE-COLLECT-SUBCASES (CDR FTY::KEYS) FTY::HAS-WILDCARD FTY::PAIRS
  FTY::CASES))))))

multicasemacro

(defmacro multicase
  (pairs &rest cases)
  (multicase-fn pairs cases))

enum-casemacro-casesfunction

(defun enum-casemacro-cases
  (kwd-alist)
  (b* (((when (atom kwd-alist)) nil) ((when (or (eq (caar kwd-alist) :otherwise)
           (eq (caar kwd-alist) :otherwise*))) `((otherwise ,(CDAR FTY::KWD-ALIST)))))
    (cons `(,(IF (ATOM (CDR FTY::KWD-ALIST))
     'OTHERWISE
     (CAAR FTY::KWD-ALIST)) ,(CDAR FTY::KWD-ALIST))
      (enum-casemacro-cases (cdr kwd-alist)))))

enumcase-case-fnfunction

(defun enumcase-case-fn
  (var-or-expr rest-args
    macro-name
    fix
    enum-members)
  (b* (((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) enum-members)) `(eq ,FTY::VAR-OR-EXPR ,(CAR FTY::REST-ARGS)))
         ((and (consp (car rest-args))
            (eq (caar rest-args) :quote)
            (true-listp (cadr rest-args))
            (subsetp (cadr rest-args) enum-members)) `(member-eq ,FTY::VAR-OR-EXPR ,(CAR FTY::REST-ARGS)))
         (t (er hard?
             macro-name
             "Bad argument: ~x0~%Must be one of ~x1 or a quoted subset."
             (car rest-args)
             enum-members)))) ((when (consp var-or-expr)) (er hard?
          macro-name
          "Expected a variable, rather than: ~x0"
          var-or-expr))
      (allowed-keywordlist-keys (append enum-members '(:otherwise :otherwise*)))
      (allowed-parenthesized-keys (append enum-members
          '(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"))
      (completep (subsetp-eq enum-members keys))
      (redundant-otherwise (and completep (member-eq :otherwise keys)))
      ((when redundant-otherwise) (er hard?
          macro-name
          "Redundant otherwise case"))
      (incompletep (and (not completep)
          (not (member-eq :otherwise keys))
          (not (member-eq :otherwise* keys))))
      ((when incompletep) (er hard?
          'macro-name
          "Incomplete cases and no :otherwise/:otherwise*"))
      (redundant-otherwise* (and completep (member-eq :otherwise* keys)))
      (case-kwd-alist (or kwd-alist (pairlis$ keys vals)))
      (case-kwd-alist (if redundant-otherwise*
          (remove-assoc-eq :otherwise* case-kwd-alist)
          case-kwd-alist))
      (body `(case (,FTY::FIX ,FTY::VAR-OR-EXPR) . ,(FTY::ENUM-CASEMACRO-CASES FTY::CASE-KWD-ALIST))))
    body))

def-enumcase-fnfunction

(defun def-enumcase-fn
  (name enum wrld)
  (b* ((tab (table-alist 'defenum-table wrld)) (look (cdr (assoc-eq enum tab)))
      (members (cdr (assoc-eq :members look)))
      (fix (cdr (assoc-eq :fix look))))
    `(defmacro ,FTY::NAME
      (var &rest rest-args)
      (enumcase-case-fn var
        rest-args
        ',FTY::NAME
        ',FTY::FIX
        ',FTY::MEMBERS))))

def-enumcasemacro

(defmacro def-enumcase
  (name enum)
  `(make-event (def-enumcase-fn ',FTY::NAME
      ',FTY::ENUM
      (w state))))

case*-keyvals-to-casesfunction

(defun case*-keyvals-to-cases
  (keyvals)
  (if (atom keyvals)
    nil
    (cons (cond ((eq (car keyvals) :otherwise*) `(t ,(CADR FTY::KEYVALS)))
        ((booleanp (car keyvals)) `((,(CAR FTY::KEYVALS)) ,(CADR FTY::KEYVALS)))
        (t `(,(CAR FTY::KEYVALS) ,(CADR FTY::KEYVALS))))
      (case*-keyvals-to-cases (cddr keyvals)))))

case*-fnfunction

(defun case*-fn
  (var keyvals)
  `(case ,FTY::VAR . ,(FTY::CASE*-KEYVALS-TO-CASES FTY::KEYVALS)))

case*macro

(defmacro case*
  (var &rest keyvals)
  (case*-fn var keyvals))

case*-equal-keyvals-to-condfunction

(defun case*-equal-keyvals-to-cond
  (var keyvals)
  (if (atom keyvals)
    nil
    (cons (if (eq (car keyvals) :otherwise*)
        `(t ,(CADR FTY::KEYVALS))
        `((equal ,FTY::VAR ,(CAR FTY::KEYVALS)) ,(CADR FTY::KEYVALS)))
      (case*-equal-keyvals-to-cond var
        (cddr keyvals)))))

case*-equal-fnfunction

(defun case*-equal-fn
  (var keyvals)
  `(cond . ,(FTY::CASE*-EQUAL-KEYVALS-TO-COND FTY::VAR FTY::KEYVALS)))

case*-equalmacro

(defmacro case*-equal
  (var &rest keyvals)
  (case*-equal-fn var keyvals))