		Search-engine friendly clone of the ACL2 documentation.

Tshell

Tshell-call-fn1

Logical story for tshell-call.

Signature
(tshell-call-fn1 cmd print save state) → (mv exit-status lines state)
Arguments: cmd — Guard (stringp cmd).; print — Guard (symbolp print).; save — Guard (booleanp save).
Returns: state — Type (state-p1 state), given (state-p1 state).

Logically, this function is defined in terms of read-ACL2-oracle. For execution, a raw lisp function is installed under-the-hood.

Definitions and Theorems

Function: tshell-call-fn1

(defun tshell-call-fn1 (cmd print save state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp cmd)
                             (symbolp print)
                             (booleanp save))))
 (declare (ignore cmd print save))
 (let ((__function__ 'tshell-call-fn1))
  (declare (ignorable __function__))
  (b*
   ((-
      (cw "Warning: under-the-hood definition of ~s0 not installed?"
          __function__))
    ((mv - exit-status state)
     (read-acl2-oracle state))
    ((mv - lines state)
     (read-acl2-oracle state)))
   (mv exit-status lines state))))

Theorem: state-p1-of-tshell-call-fn1.state

(defthm state-p1-of-tshell-call-fn1.state
  (implies (state-p1 state)
           (b* (((mv ?exit-status ?lines ?state)
                 (tshell-call-fn1 cmd print save state)))
             (state-p1 state)))
  :rule-classes :rewrite)

Theorem: state-p-of-mv-nth-2-of-tshell-call-fn1-when-state-p

(defthm state-p-of-mv-nth-2-of-tshell-call-fn1-when-state-p
  (implies
       (state-p state)
       (state-p (mv-nth 2
                        (tshell-call-fn1 cmd print save state)))))

Theorem: w-of-mv-nth-2-of-tshell-call-fn1

(defthm w-of-mv-nth-2-of-tshell-call-fn1
  (equal (w (mv-nth 2
                    (tshell-call-fn1 cmd print save state)))
         (w state)))

Subtopics

Tshell-call-unsound-fn1: Unsound variant of tshell-call-fn1 which doesn't take state.