pseudo-translate

(defun stobjs-in-list
  (stobjs-in formals)
  (if (endp formals)
    nil
    (cons (and (member (car formals) stobjs-in) (car formals))
      (stobjs-in-list stobjs-in (cdr formals)))))

(defun extend-wrld-with-fn-args-list
  (stobjs-in fn-args-lst wrld)
  (cond ((endp fn-args-lst) wrld)
    (t (let ((fn (caar fn-args-lst)) (formals (cdar fn-args-lst)))
        (putprop fn
          'symbol-class
          :common-lisp-compliant (putprop fn
            'stobjs-in
            (stobjs-in-list stobjs-in formals)
            (putprop fn
              'formals
              formals
              (extend-wrld-with-fn-args-list stobjs-in
                (cdr fn-args-lst)
                wrld))))))))

(defun translate1-cw
  (x stobjs-out bindings known-stobjs ctx w)
  (mv-let (erp msg-or-val bindings)
    (translate1-cmp x
      stobjs-out
      bindings
      known-stobjs
      ctx
      w
      (default-state-vars nil))
    (cond (erp (prog2$ (cw "~%~%ERROR in translate1-cw:  ~@0~%~%" msg-or-val)
          (mv t x bindings)))
      (t (mv nil msg-or-val bindings)))))

(defun self-bindings
  (fn-args-lst)
  (if (endp fn-args-lst)
    nil
    (acons (caar fn-args-lst)
      (caar fn-args-lst)
      (self-bindings (cdr fn-args-lst)))))

(defun pseudo-translate-defun
  (fn stobjs-in form fn-args-lst wrld)
  (let ((wrld (extend-wrld-with-fn-args-list stobjs-in fn-args-lst wrld)))
    (let ((stobjs-out (or fn t)) (bindings (self-bindings fn-args-lst)))
      (mv-let (flg val bindings)
        (translate1-cw form
          stobjs-out
          bindings
          t
          'pseudo-translate
          wrld)
        (let ((signature (and fn (cdr (assoc fn bindings)))))
          (mv flg val signature))))))

(defun pseudo-translate
  (form fn-args-lst wrld)
  (mv-let (flg val sig)
    (pseudo-translate-defun nil nil form fn-args-lst wrld)
    (declare (ignore sig))
    (mv flg val)))