		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-value

Generate a shallowly embedded ACL2 value.

Signature
(atj-gen-shallow-value value qpairs pkg-class-names curr-pkg guards$) → expr
Arguments: qpairs — Guard (cons-pos-alistp qpairs).; pkg-class-names — Guard (string-string-alistp pkg-class-names).; curr-pkg — Guard (stringp curr-pkg).; guards$ — Guard (booleanp guards$).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-shallow-value

(defun atj-gen-shallow-value
       (value qpairs pkg-class-names curr-pkg guards$)
 (declare (xargs :guard (and (cons-pos-alistp qpairs)
                             (string-string-alistp pkg-class-names)
                             (stringp curr-pkg)
                             (booleanp guards$))))
 (let ((__function__ 'atj-gen-shallow-value))
  (declare (ignorable __function__))
  (cond
   ((acl2-numberp value)
    (atj-gen-shallow-number value))
   ((characterp value)
    (atj-gen-shallow-char value guards$))
   ((stringp value)
    (atj-gen-shallow-string value guards$))
   ((symbolp value)
    (atj-gen-shallow-symbol value pkg-class-names curr-pkg guards$))
   ((consp value)
    (atj-gen-shallow-cons value qpairs))
   (t
     (prog2$ (raise "Internal error: ~x0 is not a recognized value."
                    value)
             (jexpr-name ""))))))

Theorem: jexprp-of-atj-gen-shallow-value

(defthm jexprp-of-atj-gen-shallow-value
  (b*
   ((expr (atj-gen-shallow-value value qpairs
                                 pkg-class-names curr-pkg guards$)))
   (jexprp expr))
  :rule-classes :rewrite)