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))).
