evalable-printing - ACL2 Book

other

(in-package "ACL2")

other

(program)

other

(set-state-ok t)

quote-as-neededfunction

(defun quote-as-needed
  (expr)
  (declare (xargs :guard t))
  (if (or (consp expr)
      (and (symbolp expr)
        (not (booleanp expr))
        (not (keywordp expr))))
    (list 'quote expr)
    expr))

quote-as-needed-listfunction

(defun quote-as-needed-list
  (expr-lst)
  (declare (xargs :guard (true-listp expr-lst)))
  (if (endp expr-lst)
    expr-lst
    (cons (quote-as-needed (car expr-lst))
      (quote-as-needed-list (cdr expr-lst)))))

quote-as-needed-with-stobjfunction

(defun quote-as-needed-with-stobj
  (val stobj)
  (if stobj
    stobj
    (quote-as-needed val)))

quote-as-needed-with-stobj-listfunction

(defun quote-as-needed-with-stobj-list
  (valx stobjs)
  (if (or (endp valx) (endp stobjs))
    nil
    (cons (quote-as-needed-with-stobj (car valx) (car stobjs))
      (quote-as-needed-with-stobj-list (cdr valx) (cdr stobjs)))))

*evalable-printing-abstractions*constant

(defconst *evalable-printing-abstractions*
  '(list list*-multiple list* cons))

*default-evalable-printing-abstractions*constant

(defconst *default-evalable-printing-abstractions*
  '(list list*-multiple cons))

get-evalable-printing-abstractionsfunction

(defun get-evalable-printing-abstractions
  (state)
  (if (f-boundp-global 'evalable-printing-abstractions state)
    (f-get-global 'evalable-printing-abstractions state)
    *default-evalable-printing-abstractions*))

lastcdrfunction

(defun lastcdr
  (x)
  (if (atom x)
    x
    (lastcdr (cdr x))))

make-evalable-howmutual-recursion

(mutual-recursion (defun make-evalable-how
    (val abstractions)
    (if (consp val)
      (cond ((and (member-eq 'list abstractions) (true-listp val)) (cons 'list (make-evalable-lst-how val abstractions)))
        ((or (and (member-eq 'list*-multiple abstractions)
             (consp (cdr val)))
           (member-eq 'list* abstractions)) (append (list 'list*)
            (make-evalable-lst-how val abstractions)
            (list (make-evalable-how (lastcdr val) abstractions))))
        ((member-eq 'cons abstractions) (list 'cons
            (make-evalable-how (car val) abstractions)
            (make-evalable-how (cdr val) abstractions)))
        (t (list 'quote val)))
      (quote-as-needed val)))
  (defun make-evalable-lst-how
    (val-lst abstractions)
    (if (atom val-lst)
      nil
      (cons (make-evalable-how (car val-lst) abstractions)
        (make-evalable-lst-how (cdr val-lst) abstractions)))))

make-evalable-with-stobj-howfunction

(defun make-evalable-with-stobj-how
  (val stobj abstractions)
  (if stobj
    stobj
    (make-evalable-how val abstractions)))

make-evalable-with-stobj-list-howfunction

(defun make-evalable-with-stobj-list-how
  (valx stobjs abstractions)
  (if (or (endp valx) (endp stobjs))
    nil
    (cons (make-evalable-with-stobj-how (car valx)
        (car stobjs)
        abstractions)
      (make-evalable-with-stobj-list-how (cdr valx)
        (cdr stobjs)
        abstractions))))

make-evalablemacro

(defmacro make-evalable
  (x)
  `(make-evalable-how ,X
    (get-evalable-printing-abstractions state)))

make-evalable-with-stobjsmacro

(defmacro make-evalable-with-stobjs
  (valx stobjs)
  `(make-evalable-with-stobj-list-how ,VALX
    ,STOBJS
    (get-evalable-printing-abstractions state)))