		Search-engine friendly clone of the ACL2 documentation.

Smtlink-process-user-hint

Translate-cmp-smtlink

Definitions and Theorems

Function: wrld-fn-len

(defun wrld-fn-len (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'wrld-fn-len))
    (declare (ignorable acl2::__function__))
    (b* ((world (w state)))
      (len (remove-duplicates-eq
                (strip-cadrs (universal-theory :here)))))))

Function: trans-hypothesis

(defun trans-hypothesis (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-hypothesis))
    (declare (ignorable acl2::__function__))
    (b* (((unless (and (true-listp val) (car val)))
          val)
         ((mv err term)
          (acl2::translate-cmp
               (car val)
               t t nil
               'smtlink-process-user-hint->trans-hypothesis
               (w state)
               (default-state-vars t)))
         ((when err)
          (er hard?
              'smtlink-process-user-hint->trans-hypothesis
              "Error ~
    translating form: ~q0"
              (car val))))
      (cons term (cdr val)))))

Function: trans-guard

(defun trans-guard (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-guard))
    (declare (ignorable acl2::__function__))
    (trans-hypothesis val state)))

Function: trans-more-returns

(defun trans-more-returns (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-more-returns))
    (declare (ignorable acl2::__function__))
    (b* (((unless (true-listp val)) val)
         ((unless (consp val)) val)
         ((cons first rest) val)
         (new-first (trans-hypothesis first state)))
      (cons new-first
            (trans-more-returns rest state)))))

Function: trans-argument

(defun trans-argument (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-argument))
    (declare (ignorable acl2::__function__))
    (b* (((unless (and (true-listp val)
                       (car val)
                       (cadr val)))
          val)
         ((list* name type rest) val)
         (to-be-trans (cons type (cons name 'nil)))
         ((mv err term)
          (acl2::translate-cmp
               to-be-trans t t nil
               'smtlink-process-user-hint->trans-hypothesis
               (w state)
               (default-state-vars t)))
         ((when err)
          (er hard?
              'smtlink-process-user-hint->trans-argument
              "Error ~
    translating form: ~q0"
              to-be-trans)))
      (cons name (cons (car term) rest)))))

Function: trans-formals

(defun trans-formals (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-formals))
    (declare (ignorable acl2::__function__))
    (b* (((unless (true-listp val)) val)
         ((unless (consp val)) val)
         ((cons first rest) val)
         (new-first (trans-argument first state)))
      (cons new-first (trans-formals rest state)))))

Function: trans-returns

(defun trans-returns (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-returns))
    (declare (ignorable acl2::__function__))
    (b* (((unless (true-listp val)) val)
         ((unless (consp val)) val)
         ((cons first rest) val)
         (new-first (trans-argument first state)))
      (cons new-first (trans-formals rest state)))))

Function: trans-func-option

(defun trans-func-option (opt val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-func-option))
    (declare (ignorable acl2::__function__))
    (cond ((equal opt ':formals)
           (trans-formals val state))
          ((equal opt ':returns)
           (trans-returns val state))
          ((equal opt ':guard)
           (trans-guard val state))
          ((equal opt ':more-returns)
           (trans-more-returns val state))
          (t val))))

Function: trans-function

(defun trans-function (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-function))
    (declare (ignorable acl2::__function__))
    (b* (((unless (and (true-listp val) (consp val)))
          val)
         ((list* first second rest) val)
         (new-second (trans-func-option first second state))
         (new-functions (cons first
                              (cons new-second
                                    (trans-function rest state)))))
      new-functions)))

Function: trans-functions

(defun trans-functions (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-functions))
    (declare (ignorable acl2::__function__))
    (b* (((unless (true-listp val)) val)
         ((unless (consp val)) val)
         ((cons first rest) val)
         ((cons fname options) first)
         (new-first (cons fname (trans-function options state))))
      (cons new-first
            (trans-functions rest state)))))

Function: trans-hypotheses

(defun trans-hypotheses (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-hypotheses))
    (declare (ignorable acl2::__function__))
    (b* (((unless (true-listp val)) val)
         ((unless (consp val)) val)
         ((cons first rest) val)
         (new-first (trans-hypothesis first state)))
      (cons new-first
            (trans-hypotheses rest state)))))

Function: trans-hint-option

(defun trans-hint-option (opt val state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'trans-hint-option))
  (declare (ignorable acl2::__function__))
  (cond
   ((equal opt ':functions)
    (trans-functions val state))
   ((equal opt ':hypotheses)
    (trans-hypotheses val state))
   ((equal opt ':wrld-len)
    (er
     hard?
     'smtlink-process-user-hint->trans-hint-option
     "User trying to access internal parameter ~
                wrld-len!"))
   (t val))))

Function: trans-hint

(defun trans-hint (hint state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'trans-hint))
   (declare (ignorable acl2::__function__))
   (b* (((unless (true-listp hint)) hint)
        (wrld-len (wrld-fn-len state))
        ((if (atom hint))
         (cons ':wrld-len (cons wrld-len 'nil)))
        ((unless (cdr hint)) hint)
        ((list* first second rest) hint)
        (new-second (trans-hint-option first second state))
        (new-hint (cons first
                        (cons new-second (trans-hint rest state)))))
     new-hint)))

Subtopics

Trans-argument
Trans-hypothesis
Trans-more-returns
Trans-hypotheses
Trans-hint-option
Trans-hint
Trans-functions
Trans-function
Trans-func-option
Wrld-fn-len
Trans-returns
Trans-formals
Trans-guard