with-quoted-forms - ACL2 Book

Included Books

bstar

other

(in-package "ACL2")

include-book

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

alistp-pairlis$theorem

(defthm alistp-pairlis$ (alistp (pairlis$ a b)))

beta-reduce-with-quotesmutual-recursion

(mutual-recursion (defun beta-reduce-with-quotes
    (x alist)
    (declare (xargs :guard (and (pseudo-termp x) (alistp alist))))
    (cond ((eq x nil) nil)
      ((atom x) (let ((look (assoc x alist)))
          (if look
            (cdr look)
            x)))
      ((eq (car x) 'quote) x)
      ((eq (car x) 'fq) (cons 'quote (beta-reduce-with-quotes-list (cdr x) alist)))
      ((symbolp (car x)) (cons (car x) (beta-reduce-with-quotes-list (cdr x) alist)))
      (t (beta-reduce-with-quotes (caddar x)
          (pairlis$ (cadar x)
            (beta-reduce-with-quotes-list (cdr x) alist))))))
  (defun beta-reduce-with-quotes-list
    (x alist)
    (declare (xargs :guard (and (pseudo-term-listp x) (alistp alist))))
    (if (atom x)
      nil
      (cons (beta-reduce-with-quotes (car x) alist)
        (beta-reduce-with-quotes-list (cdr x) alist)))))

fqfunction

(defun fq (x) x)

with-quoted-forms-fnfunction

(defun with-quoted-forms-fn
  (form state)
  (declare (xargs :mode :program :stobjs state))
  (b* (((er trans) (translate form
         t
         nil
         nil
         'with-quoted-var-terms
         (w state)
         state)) (reduce (beta-reduce-with-quotes trans nil))
      ((er (cons & val)) (simple-translate-and-eval reduce
          nil
          nil
          "Term for with-quoted-forms"
          'with-quoted-var-terms
          (w state)
          state
          t)))
    (value val)))

with-quoted-formsmacro

(defmacro with-quoted-forms
  (form)
  `(with-quoted-forms-fn ',FORM state))

var-fq-bindings-lstfunction

(defun var-fq-bindings-lst
  (vars)
  (if (atom vars)
    nil
    (cons ``(,',(CAR VARS) ,(FQ ,(CAR VARS)))
      (var-fq-bindings-lst (cdr vars)))))

var-fq-bindingsmacro

(defmacro var-fq-bindings
  (vars)
  (cons 'list (var-fq-bindings-lst vars)))

beta-reduce-collect-bindingsmutual-recursion

(mutual-recursion (defun beta-reduce-collect-bindings
    (x alist bindings)
    (declare (xargs :guard (and (pseudo-termp x) (alistp alist))
        :mode :program))
    (cond ((eq x nil) (mv nil bindings))
      ((atom x) (let ((look (assoc x alist)))
          (mv (if look
              (cdr look)
              x)
            bindings)))
      ((eq (car x) 'quote) (mv x bindings))
      (t (mv-let (lst bindings)
          (beta-reduce-collect-bindings-list (cdr x) alist bindings)
          (if (symbolp (car x))
            (mv (cons (car x) lst) bindings)
            (let ((new-bindings (pairlis$ (cadar x) lst)))
              (beta-reduce-collect-bindings (caddar x)
                new-bindings
                (append new-bindings bindings))))))))
  (defun beta-reduce-collect-bindings-list
    (x alist bindings)
    (declare (xargs :guard (and (pseudo-term-listp x) (alistp alist))))
    (if (atom x)
      (mv nil bindings)
      (b* (((mv car bindings) (beta-reduce-collect-bindings (car x) alist bindings)) ((mv cdr bindings) (beta-reduce-collect-bindings-list (cdr x) alist bindings)))
        (mv (cons car cdr) bindings)))))

bind-according-to-alist-lstfunction

(defun bind-according-to-alist-lst
  (vars alist)
  (if (atom vars)
    nil
    (cons `(,(CAR VARS) (cdr (assoc ',(CAR VARS) ,ALIST)))
      (bind-according-to-alist-lst (cdr vars) alist))))

bind-according-to-alistmacro

(defmacro bind-according-to-alist
  (alist vars &rest body)
  `(let ,(BIND-ACCORDING-TO-ALIST-LST VARS ALIST) . ,BODY))

bind-as-in-definition-fnfunction

(defun bind-as-in-definition-fn
  (fn-or-call vars term)
  `(b* ((fn-or-call ',FN-OR-CALL) (fn (if (consp fn-or-call)
          (car fn-or-call)
          fn-or-call))
      (body (getprop fn
          'unnormalized-body
          nil
          'current-acl2-world
          (w state)))
      (alist (and (consp fn-or-call)
          (pairlis$ (fgetprop fn 'formals nil (w state))
            (cdr fn-or-call))))
      ((mv & bindings) (beta-reduce-collect-bindings body alist alist)))
    (bind-according-to-alist bindings ,VARS . ,TERM)))

bind-as-in-definitionmacro

(defmacro bind-as-in-definition
  (fn vars &rest term)
  (bind-as-in-definition-fn fn vars term))