From 092176848cbfd27b96c323cc30c54dff4c4a6872 Mon Sep 17 00:00:00 2001 From: Camm Maguire Date: Mon, 8 May 2017 12:58:52 -0400 Subject: Import acl2_7.4dfsg.orig.tar.gz [dgit import orig acl2_7.4dfsg.orig.tar.gz] --- .../tiny-fib-example/with-copy-of-stobj.lsp | 38 ++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp (limited to 'books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp') diff --git a/books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp new file mode 100644 index 0000000..5aa1d0f --- /dev/null +++ b/books/workshops/2004/matthews-vroon/support/tiny-fib-example/with-copy-of-stobj.lsp @@ -0,0 +1,38 @@ +(defmacro with-copy-of-stobj (stobj mv-let-form) + (let ((copy-from-stobj (join-symbols stobj 'copy-from- stobj)) + (copy-to-stobj (join-symbols stobj 'copy-to- stobj))) + `(let ((stobj (,copy-from-stobj ,stobj))) + (with-local-stobj + ,stobj + (mv-let ,(nth 1 mv-let-form) + (let ((,stobj (,copy-to-stobj stobj ,stobj))) + ,(nth 2 mv-let-form)) + ,(nth 3 mv-let-form)))))) + +(defun steps-to-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (let ((steps (steps-to-cutpoint-tail 0 (copy-from-tiny-state tiny-state)))) + (if (and (natp steps) ;the number of steps is a natural number + (with-copy-of-stobj + tiny-state + (mv-let (result tiny-state) + (let ((tiny-state (run steps tiny-state))) + (mv (at-cutpoint tiny-state) tiny-state)) + result))) + steps + (omega)))) + +(defun steps-to-cutpoint (tiny-state) + (declare (xargs :stobjs (tiny-state))) + (let ((steps (steps-to-cutpoint-tail 0 (copy-from-tiny-state tiny-state)))) + (if (and (natp steps) ;the number of steps is a natural number + (let ((ts (copy-from-tiny-state tiny-state))) ;all of this is to see if + (with-local-stobj ;we're at a cutpoint + tiny-state ;if we run the machine for + (mv-let (result tiny-state) ;steps steps + (let* ((tiny-state (copy-to-tiny-state ts tiny-state)) + (tiny-state (run steps tiny-state))) + (mv (at-cutpoint tiny-state) tiny-state)) + result)))) + steps + (omega)))) \ No newline at end of file -- cgit v1.2.3