term-patterns - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "meta/pseudo-termp-lemmas" :dir :system)

get-term-patternsmacro

(defmacro get-term-patterns
  (name)
  `(cdr (assoc ',NAME (table-alist 'term-patterns world))))

set-term-patternsmacro

(defmacro set-term-patterns
  (name val)
  `(table term-patterns ',NAME ,VAL))

add-term-patternmacro

(defmacro add-term-pattern
  (name val)
  `(set-term-patterns ,NAME
    (cons ',VAL (get-term-patterns ,NAME))))

add-term-patternsmacro

(defmacro add-term-patterns
  (name &rest vals)
  `(set-term-patterns ,NAME
    (append ',VALS (get-term-patterns ,NAME))))

fn-patfunction

(defun fn-pat (fn) (declare (xargs :guard t)) `(,FN . &))

fn-patsfunction

(defun fn-pats
  (fns)
  (declare (xargs :guard t))
  (if (atom fns)
    nil
    (cons (fn-pat (car fns)) (fn-pats (cdr fns)))))

add-fn-term-patternmacro

(defmacro add-fn-term-pattern
  (name fn)
  `(set-term-patterns ,NAME
    (cons ',(FN-PAT FN) (get-term-patterns ,NAME))))

add-fn-term-patternsmacro

(defmacro add-fn-term-patterns
  (name &rest fns)
  `(set-term-patterns ,NAME
    (append ',(FN-PATS FNS) (get-term-patterns ,NAME))))

term-patternpmutual-recursion

(mutual-recursion (defun term-patternp
    (x)
    (declare (xargs :guard t))
    (cond ((atom x) t)
      ((eq (car x) 'quote) t)
      (t (and (symbolp (car x)) (term-pattern-listp (cdr x))))))
  (defun term-pattern-listp
    (x)
    (if (atom x)
      (or (eq x nil) (eq x '&))
      (and (term-patternp (car x)) (term-pattern-listp (cdr x))))))

term-pattern-matchmutual-recursion

(mutual-recursion (defun term-pattern-match
    (x pat acc)
    (declare (xargs :guard (and (term-patternp pat) (alistp acc))
        :verify-guards nil))
    (cond ((eq pat '&) acc)
      ((and (symbolp pat) (not (booleanp pat))) (let ((look (assoc pat acc)))
          (if look
            (and (equal x (cdr look)) acc)
            (cons (cons pat x) acc))))
      ((atom pat) (case-match x (('quote !pat) acc)))
      ((eq (car pat) 'quote) (and (equal x pat) acc))
      (t (and (consp x)
          (eq (car x) (car pat))
          (term-pattern-match-list (cdr x) (cdr pat) acc)))))
  (defun term-pattern-match-list
    (x pat acc)
    (declare (xargs :guard (and (term-pattern-listp pat) (alistp acc))))
    (if (atom pat)
      (cond ((eq pat '&) acc) (t (and (eq x nil) acc)))
      (and (consp x)
        (let ((acc (term-pattern-match (car x) (car pat) acc)))
          (and acc (term-pattern-match-list (cdr x) (cdr pat) acc)))))))

include-book

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

other

(make-flag term-pattern-match-flag term-pattern-match)

other

(defthm-term-pattern-match-flag term-pattern-match-flag-alistp
  (term-pattern-match (implies (alistp acc)
      (alistp (term-pattern-match x pat acc)))
    :name term-pattern-match-alistp)
  (term-pattern-match-list (implies (alistp acc)
      (alistp (term-pattern-match-list x pat acc)))
    :name term-pattern-match-list-alistp)
  :hints (("goal" :induct (term-pattern-match-flag flag x pat acc))))

other

(verify-guards term-pattern-match)

other

(defthm-term-pattern-match-flag term-pattern-match-flag-pseudo-term-substp
  (term-pattern-match (implies (and (pseudo-termp x) (pseudo-term-substp acc))
      (pseudo-term-substp (term-pattern-match x pat acc)))
    :name term-pattern-match-pseudo-term-substp)
  (term-pattern-match-list (implies (and (pseudo-term-listp x) (pseudo-term-substp acc))
      (pseudo-term-substp (term-pattern-match-list x pat acc)))
    :name term-pattern-match-list-pseudo-term-substp)
  :hints (("goal" :induct (term-pattern-match-flag flag x pat acc))))

match-term-patternfunction

(defun match-term-pattern
  (x pats)
  (declare (xargs :guard (term-pattern-listp pats)))
  (if (atom pats)
    nil
    (or (term-pattern-match x (car pats) '((& . &)))
      (match-term-pattern x (cdr pats)))))

pseudo-term-substp-match-term-patterntheorem

(defthm pseudo-term-substp-match-term-pattern
  (implies (pseudo-termp x)
    (pseudo-term-substp (match-term-pattern x pats))))

term-matchesfunction

(defun term-matches
  (term name world)
  (match-term-pattern term
    (cdr (assoc name (table-alist 'term-patterns world)))))

pseudo-term-substp-term-matchestheorem

(defthm pseudo-term-substp-term-matches
  (implies (pseudo-termp x)
    (pseudo-term-substp (term-matches x name world))))

in-theory

(in-theory (disable match-term-pattern term-pattern-match term-matches))