Filtering...

untranslate-for-exec-tests

books/tools/untranslate-for-exec-tests

Included Books

untranslate-for-exec
other
(in-package "ACL2")
include-book
(include-book "untranslate-for-exec")
assert-same-stobjs-outmacro
(defmacro assert-same-stobjs-out
  (old-fn new-fn)
  `(make-event (b* ((world (w state)) (old-stobjs-out (getprop ',OLD-FN 'stobjs-out nil 'current-acl2-world world))
        (new-stobjs-out (getprop ',NEW-FN 'stobjs-out nil 'current-acl2-world world))
        ((when (equal old-stobjs-out new-stobjs-out)) (value '(value-triple :success))))
      (er soft
        ',NEW-FN
        "Stobjs-out mismatch: expected ~x0, found ~x1.~%"
        old-stobjs-out
        new-stobjs-out))))
rebuild-function-fnfunction
(defun rebuild-function-fn
  (fn world)
  (b* ((new-fn (intern-in-package-of-symbol (concatenate 'string (symbol-name fn) "-NEW")
         fn)) (new-fn-correct (intern-in-package-of-symbol (concatenate 'string (symbol-name new-fn) "-CORRECT")
          fn))
      (body (getprop fn
          'unnormalized-body
          nil
          'current-acl2-world
          world))
      (formals (getprop fn 'formals nil 'current-acl2-world world))
      (stobjs-out (getprop fn 'stobjs-out nil 'current-acl2-world world))
      (- (cw "Original body:  ~x0~%" body))
      ((mv errmsg new-body) (untranslate-for-execution body stobjs-out world))
      ((when errmsg) (er hard?
          'rebuild-function
          "Error with untranslate-for-execution for ~x0: ~@1.~%"
          fn
          errmsg))
      (- (cw "Rewritten body: ~x0~%" new-body)))
    `(progn (defun ,NEW-FN ,FORMALS ,NEW-BODY)
      (defthm ,NEW-FN-CORRECT
        (equal (,NEW-FN . ,FORMALS) (,FN . ,FORMALS)))
      (assert-same-stobjs-out ,FN ,NEW-FN))))
rebuild-functionmacro
(defmacro rebuild-function
  (fn)
  `(make-event (rebuild-function-fn ',FN (w state))))
f1function
(defun f1 nil 5)
other
(rebuild-function f1)
f2function
(defun f2 (x) x)
other
(rebuild-function f2)
f3function
(defun f3 (x) (list x x))
other
(rebuild-function f3)
f4function
(defun f4 (x) (mv x x))
other
(rebuild-function f4)
f5function
(defun f5
  (x)
  (let ((y x))
    y))
other
(rebuild-function f5)
f6function
(defun f6
  (x)
  (let* ((y x) (z y))
    (+ y z)))
other
(rebuild-function f6)
f7function
(defun f7 (x) (f4 x))
other
(rebuild-function f7)
f8function
(defun f8
  (x)
  (if x
    (f4 x)
    (mv x x)))
other
(rebuild-function f8)
f9function
(defun f9
  (x)
  (cond ((equal x 1) (f4 x))
    ((equal x 2) (mv 1 2))
    (t (mv x 3))))
other
(rebuild-function f9)
other
(set-ignore-ok t)
f10function
(defun f10
  (x)
  (cond ((equal x 1) (let ((x 1))
        (f4 x)))
    ((equal x 2) (mv-let (x y) (f4 6) (mv 1 2)))
    (t (mv x 3))))
other
(rebuild-function f10)
f11function
(defun f11 (x) (mv-let (a b c) (mv 1 2 x) (mv (+ a b c) x)))
other
(rebuild-function f11)
f12function
(defun f12 (x) (mv 1 2 x 3))
other
(rebuild-function f12)
f13function
(defun f13 (x y) (mv-let (a b) (mv y x) (mv a b x)))
other
(rebuild-function f13)
f13function
(defun f13 (x y) (mv-let (a b) (mv y x) (mv a b x)))
other
(rebuild-function f13)
f14function
(defun f14 (x y) (mv (mv-let (a b) (mv x y) (+ a b)) y))
other
(rebuild-function f14)
f14function
(defun f14 (x y) (mv (mv-let (a b) (mv x y) (+ a b)) y))
other
(rebuild-function f14)
f15function
(defun f15 (x y) (mv (mv-let (a b) (mv x y) (+ a b x)) y))
other
(rebuild-function f15)
f16function
(defun f16
  (x y)
  (let ((a (+ x y)))
    (mv-let (b c) (mv y x) (+ a b c))))
other
(rebuild-function f16)
f17function
(defun f17
  (x y)
  (let ((a (+ x y)))
    (mv-let (a c) (mv y a) (+ a x c))))
other
(rebuild-function f17)
f18function
(defun f18 (x) (mv-let (y z) (f4 x) (mv x y)))
other
(rebuild-function f18)
f19function
(defun f19
  (x)
  (let ((y (f2 x)))
    (mv-let (y z)
      (f4 y)
      (mv-let (a b c)
        (mv z y x)
        (mv-let (w x y z) (f12 a) (mv a b c w x y z))))))
other
(rebuild-function f19)