# Untranslate-for-execution

Attempt to do a kind of untranslation of a ute-term-p in
order to restore any mv-let and mv forms, ideally so that the
term can be executed.

- Signature
(untranslate-for-execution x stobjs-out world)
→
(mv errmsg new-x)

- Arguments
`x` — The term to untranslate.

Guard (ute-term-p x).
`stobjs-out` — The expected stobjs-out for this term.

Guard (and (symbol-listp stobjs-out) (consp stobjs-out)).
`world` — The current ACL2 world, needed for signature lookups.

Guard (plist-worldp world).
- Returns
`errmsg` — NIL on success or an error msg on failure.
`new-x` — New version of x, with MVs restored.

When terms are translated into ute-term-ps,
information about their mv and stobj nature can be lost. For
instance, suppose we start with a simple definition, f:

(defun f (a b) (mv a b))

Since mv is logically just list, the logical definition of
f ends up being (cons a (cons b 'nil)). Suppose we want to use this
logical definition to derive some new function, g,

(defun g (a b) (cons a (cons b 'nil)))

Although f and g are logically identical, they are practically
incompatible: f returns two values but g only returns one. This kind
of mismatch can sometimes cause problems when you are writing code that
modifies existing ACL2 functions.

The untranslate-for-execution tool tries to allow you to recover
something like the true original definition. For example, if we run:

(untranslate-for-execution
'(cons a (cons b 'nil)) ;; unnormalized-body property of F
'(nil nil) ;; stobjs-out property of F
(w state))

Then we get back (mv a b), i.e., the cons nest has been
``properly'' converted back into an mv form.

In general, we try to ``smartly'' walk through the term and restore mv and mv-let forms throughout it. However, note that this is an
experimental tool and it may not yet be particularly robust.

### Definitions and Theorems

**Function: **untranslate-for-execution

(defun untranslate-for-execution (x stobjs-out world)
(declare (xargs :guard (and (ute-term-p x)
(and (symbol-listp stobjs-out)
(consp stobjs-out))
(plist-worldp world))))
(let ((__function__ 'untranslate-for-execution))
(declare (ignorable __function__))
(b* (((mv err x-fix1)
(reincarnate-mvs x world))
((when err) (mv err x))
(n (len stobjs-out))
((when (eql n 1)) (mv nil x-fix1))
((mv err new-x)
(convert-subexpression-to-mv n x-fix1 world))
((when err) (mv err x)))
(mv nil new-x))))

### Subtopics

- Convert-subexpression-to-mv
- Rewrite an expression that occurs a multiply valued context to make
its multiple returns explicit.
- Ute-term-p
- Recognize the kinds of terms that can be processed by untranslate-for-execution.
- Reincarnate-mvs
- Try to convert translated MV forms back into their MV-LET/MV form.
- Match-cons-nest
- Matches (cons x1 (cons ... (cons xn 'nil))).