untranslate-for-exec

(in-package "ACL2")

(defines ute-term-p
  :parents (untranslate-for-execution)
  :short "Recognize the kinds of terms that can be processed by @(see
untranslate-for-execution)."
  :long "<p>These are similar to @(see pseudo-termp)s, but we also explicitly
support @(see mv-let) and @(see mv) forms.</p>"
  :flag-local nil
  (define ute-term-p
    (x)
    :flag :term (cond ((atom x) (symbolp x))
      ((eq (car x) 'quote) (and (consp (cdr x)) (null (cdr (cdr x)))))
      ((not (true-listp x)) nil)
      ((eq (car x) 'if) (and (eql (len (cdr x)) 3) (ute-termlist-p (cdr x))))
      ((eq (car x) 'mv-let) (and (eql (len (cdr x)) 3)
          (b* (((list vars expr body) (cdr x)))
            (and (symbol-listp vars)
              (ute-term-p expr)
              (ute-term-p body)))))
      ((not (ute-termlist-p (cdr x))) nil)
      (t (or (symbolp (car x))
          (and (true-listp (car x))
            (eql (len (car x)) 3)
            (b* (((list lambda vars body) (car x)))
              (and (eq lambda 'lambda)
                (symbol-listp vars)
                (ute-term-p body)
                (equal (len vars) (len (cdr x))))))))))
  (define ute-termlist-p
    (x)
    :flag :list (if (atom x)
      (not x)
      (and (ute-term-p (car x)) (ute-termlist-p (cdr x)))))
  ///
  (defthm ute-termlist-p-when-atom
    (implies (atom x) (equal (ute-termlist-p x) (not x)))
    :hints (("Goal" :expand ((ute-termlist-p x)))))
  (defthm ute-termlist-p-of-cons
    (equal (ute-termlist-p (cons a x))
      (and (ute-term-p a) (ute-termlist-p x)))
    :hints (("Goal" :expand ((ute-termlist-p (cons a x))))))
  (defthm true-listp-when-ute-termlist-p
    (implies (ute-termlist-p x) (true-listp x))
    :rule-classes :compound-recognizer :hints (("Goal" :induct (len x))))
  (defthm ute-term-p-of-car-when-ute-termlist-p
    (implies (ute-termlist-p x) (ute-term-p (car x))))
  (defthm ute-termlist-p-of-cdr-when-ute-termlist-p
    (implies (ute-termlist-p x) (ute-termlist-p (cdr x))))
  (defthm ute-termlist-p-of-append
    (equal (ute-termlist-p (append x y))
      (and (ute-termlist-p (list-fix x)) (ute-termlist-p y)))
    :hints (("Goal" :induct (len x))))
  (defthm ute-termlist-p-of-rev
    (equal (ute-termlist-p (rev x))
      (ute-termlist-p (list-fix x)))
    :hints (("Goal" :induct (len x)))))

(define match-ascending-mv-nth-list-aux
  ((x ute-termlist-p "Possibly a list of MV-NTHs.") (n natp
      "Current index we expect to match, e.g., starts with 0.")
    (rhs ute-term-p "RHS we expect to match, e.g., 'mv."))
  :returns (rest ute-termlist-p
    :hyp (ute-termlist-p x)
    "Whatever comes after the (mv-nth ...) list.")
  (b* (((when (atom x)) x) (term1 (car x))
      ((unless (and (equal (len term1) 3)
           (equal (first term1) 'mv-nth)
           (equal (second term1) (list 'quote n))
           (equal (third term1) rhs))) x))
    (match-ascending-mv-nth-list-aux (cdr x) (+ n 1) rhs)))

(define match-ascending-mv-nth-list
  ((x ute-termlist-p "Possibly a list of MV-NTHs.") (rhs ute-term-p "RHS we expect to match."))
  :returns (rest ute-termlist-p :hyp (ute-termlist-p x))
  (match-ascending-mv-nth-list-aux x 0 rhs))

(define match-cons-nest-aux
  ((x ute-term-p) (acc ute-termlist-p))
  :parents (match-cons-nest)
  :returns (mv (matchp booleanp :rule-classes :type-prescription)
    (acc ute-termlist-p :hyp :guard))
  (cond ((atom x) (mv nil acc))
    ((equal x ''nil) (mv t acc))
    ((and (eq (car x) 'cons) (equal (length x) 3)) (match-cons-nest-aux (third x) (cons (second x) acc)))
    (t (mv nil acc)))
  ///
  (defthm true-listp-of-match-cons-nest-aux
    (implies (true-listp acc)
      (true-listp (mv-nth 1 (match-cons-nest-aux x acc))))))

(define match-cons-nest
  ((x ute-term-p))
  :parents (untranslate-for-execution)
  :short "Matches @('(cons x1 (cons ... (cons xn 'nil)))')."
  :returns (mv (matchp booleanp :rule-classes :type-prescription)
    (args ute-termlist-p :hyp :guard))
  (if (and (consp x) (eq (car x) 'cons))
    (mv-let (matchp acc)
      (match-cons-nest-aux x nil)
      (mv matchp (rev acc)))
    (mv nil nil)))

(define patmatch-mv-style-lambda
  ((x ute-term-p "Should be a lambda."))
  :guard (and (consp x) (consp (car x)))
  :returns (mv (matchp booleanp
      :rule-classes :type-prescription "True if this looks like an MV-LET lambda, NIL
                        if it looks like some other kind of lambda.")
    (vars "On match, the variables bound in this mv-let."
      (implies (ute-term-p x) (symbol-listp vars)))
    (expr "On match, the multiply valued expression to bind
                        to these variables.  MVs not yet reincarnated."
      (implies (and match (ute-term-p x)) (ute-term-p expr)))
    (body "On match, the inner body of this mv-let."
      (implies (and matchp (ute-term-p x)) (ute-term-p body))))
  (b* (((list & top-formals top-body) (car x)) ((unless (and (consp top-formals)
           (eq (car top-formals) 'mv)
           (consp top-body)
           (consp (car top-body)))) (mv nil nil nil nil))
      ((list & inner-formals inner-body) (car top-body))
      (inner-args (cdr top-body))
      (post-mv (cdr top-formals))
      (post-inner-args (match-ascending-mv-nth-list inner-args 'mv))
      ((unless (equal post-mv post-inner-args)) (mv nil nil nil nil))
      (mv-vars (butlast inner-formals (len post-mv))))
    (mv t mv-vars (second x) inner-body))
  :prepwork ((local (defthm symbol-listp-of-butlast
       (implies (symbol-listp x) (symbol-listp (butlast x n)))
       :hints (("Goal" :in-theory (enable butlast))))))
  ///
  (defret acl2-count-of-patmatch-mv-style-lambda-new-body
    (implies matchp (< (acl2-count body) (acl2-count x)))
    :rule-classes ((:rewrite) (:linear))))

(define convert-subexpression-to-mv
  :parents (untranslate-for-execution)
  :short "Rewrite an expression that occurs a multiply valued context to make
          its multiple returns explicit."
  ((n natp "Number of return values this expression has.") (x ute-term-p "The expression to rewrite.")
    (world plist-worldp "World, for return-value checking."))
  :guard (<= 2 n)
  :returns (mv (errmsg "NIL on success, or an error @(see msg) on failure.")
    (new-x ute-term-p :hyp (ute-term-p x)))
  (b* (((when (atom x)) (mv (msg "Expected ~x0 return values, found ~x1." n x) x)) ((when (fquotep x)) (mv (msg "Expected ~x0 return values, found ~x1." n x) x))
      (fn (first x))
      (args (rest x))
      ((when (consp fn)) (b* (((list & formals body) (first x)) ((mv err body) (convert-subexpression-to-mv n body world))
            ((when err) (mv err x))
            (new-x (cons (list 'lambda formals body) (cdr x))))
          (mv nil new-x)))
      ((when (eq fn 'if)) (b* (((list test then else) args) ((mv err1 then) (convert-subexpression-to-mv n then world))
            ((when err1) (mv (msg "> In then branch of ~x0:~%~@1~%" test err1) x))
            ((mv err2 else) (convert-subexpression-to-mv n else world))
            ((when err2) (mv (msg "> In else branch of ~x0:~%~@1~%" else err2) x))
            (new-x (list 'if test then else)))
          (mv nil new-x)))
      ((when (eq fn 'mv-let)) (b* (((list vars expr body) args) ((mv err1 body) (convert-subexpression-to-mv n body world))
            ((when err1) (mv (msg "> In body of mv-let binding ~x0:~%~@1~%" vars err1)
                x))
            (new-x (list 'mv-let vars expr body)))
          (mv nil new-x)))
      ((when (eq fn 'cons)) (b* (((mv matchp cons-args) (match-cons-nest x)) ((unless matchp) (mv (msg "Expected ~x0 return values, found ~x1.~%" n x) x))
            ((unless (equal (len cons-args) n)) (mv (msg "Expected ~x0 return values, but found cons nest of size ~x1: ~x2~%"
                  n
                  (len cons-args)
                  x)
                x))
            (new-x (cons 'mv cons-args)))
          (mv nil new-x)))
      (stobjs-out (getprop fn 'stobjs-out :bad 'current-acl2-world world))
      ((when (eq stobjs-out :bad)) (mv (msg "Don't know :stobjs-out of ~x0.~%" fn) x))
      ((unless (equal (len stobjs-out) n)) (mv (msg "Expected ~x0 return values, but ~x1 returns ~x2 values."
            n
            (car x)
            (len stobjs-out))
          x)))
    (mv nil x)))

(defines reincarnate-mvs
  :parents (untranslate-for-execution)
  :short "Try to convert translated MV forms back into their MV-LET/MV form."
  :returns-hints (("Goal" :expand ((ute-term-p x))))
  (define reincarnate-mvs
    ((x ute-term-p "The term to try to untranslate.") (world plist-worldp
        "The world, needed for stobjs-out lookups."))
    :returns (mv (errmsg "NIL on success or an error @(see msg) on failure.")
      (new-x "New version of @('x') with MVs restored."
        (implies (ute-term-p x) (ute-term-p new-x))))
    (b* (((when (atom x)) (mv nil x)) ((when (fquotep x)) (mv nil x))
        ((cons fn args) x)
        ((when (eq fn 'mv-let)) (b* (((list vars expr body) args) ((mv err expr) (reincarnate-mvs expr world))
              ((when err) (mv err x))
              ((mv err body) (reincarnate-mvs body world))
              ((when err) (mv err x))
              (new-x (list 'mv-let vars expr body)))
            (mv nil new-x)))
        ((when (symbolp fn)) (b* (((mv err args) (reincarnate-mvs-list args world)) ((when err) (mv err x))
              (new-x (cons fn args)))
            (mv nil new-x)))
        ((mv matchp mv-vars mv-expr mv-body) (patmatch-mv-style-lambda x))
        ((unless matchp) (b* (((list & formals body) fn) ((mv err args) (reincarnate-mvs-list args world))
              ((when err) (mv err x))
              ((mv err body) (reincarnate-mvs body world))
              ((when err) (mv err x))
              (new-x (cons (list 'lambda formals body) args)))
            (mv nil new-x)))
        (num-vars (len mv-vars))
        ((unless (<= 2 num-vars)) (mv (msg "MV-LET style lambda has only one variable? ~x0~%" x)
            x))
        ((mv err mv-expr) (convert-subexpression-to-mv num-vars mv-expr world))
        ((when err) (mv err x))
        ((mv err mv-body) (reincarnate-mvs mv-body world))
        ((when err) (mv err x))
        (new-expr (list 'mv-let mv-vars mv-expr mv-body)))
      (mv nil new-expr)))
  (define reincarnate-mvs-list
    ((x ute-termlist-p "The terms to try to untranslate.") (world plist-worldp
        "The world, needed for stobjs-out lookups."))
    :returns (mv (errmsg "NIL on success or an error @(see msg) on failure.")
      (new-x "New version of @('x') with MVs restored."
        (and (implies (ute-termlist-p x) (ute-termlist-p new-x))
          (equal (len new-x) (len x)))))
    (b* (((when (atom x)) (mv nil nil)) ((mv err1 car) (reincarnate-mvs (car x) world))
        ((when err1) (mv err1 x))
        ((mv err2 cdr) (reincarnate-mvs-list (cdr x) world))
        ((when err2) (mv err2 x)))
      (mv nil (cons car cdr)))))

(define untranslate-for-execution
  :parents (macros)
  :short "Attempt to do a kind of untranslation of a @(see ute-term-p) in
order to restore any @(see mv-let) and @(see mv) forms, ideally so that the
term can be executed."
  ((x "The term to untranslate." ute-term-p) (stobjs-out "The expected stobjs-out for this term."
      (and (symbol-listp stobjs-out) (consp stobjs-out)))
    (world "The current ACL2 world, needed for signature lookups."
      plist-worldp))
  :returns (mv (errmsg "NIL on success or an error @(see msg) on failure.")
    (new-x "New version of @('x'), with MVs restored."))
  :long "<p>When @(see term)s are translated into @(see ute-term-p)s,
information about their @(see mv) and @(see stobj) nature can be lost.  For
instance, suppose we start with a simple definition, @('f'):</p>

@({
     (defun f (a b) (mv a b))
})

<p>Since @(see mv) is logically just @(see 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'),</p>

@({
     (defun g (a b) (cons a (cons b 'nil)))
})

<p>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.</p>

<p>The @('untranslate-for-execution') tool tries to allow you to recover
something like the true original definition.  For example, if we run:</p>

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

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

<p>In general, we try to ``smartly'' walk through the term and restore @(see
mv) and @(see mv-let) forms throughout it.  However, note that this is an
experimental tool and it may not yet be particularly robust.</p>"
  (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)))