From c3ddaf8b8bce2f9f44226249393ab2f12c6d82de Mon Sep 17 00:00:00 2001
From: Tim Daly <daly@axiom-developer.org>
Date: Wed, 15 Jul 2015 15:52:54 -0400
Subject: [PATCH] books/bookvol5: Use ACL2 to prove isWrapped function

Goal: Prove Axiom correct

This is the first example of using ACL2 against the Axiom
common lisp code to prove the function correct. The signature
for isWrapped is

   isWrapped: t -> (or t nil)

It is a predicate that takes any argument and returns either t or nil.
---
 books/bookvol5.pamphlet         |   26 +++++++++++++++++++++++++-
 changelog                       |    3 +++
 patch                           |   14 +++++++++-----
 src/axiom-website/patches.html  |    2 ++
 src/interp/i-util.lisp.pamphlet |    6 ------
 5 files changed, 39 insertions(+), 12 deletions(-)

diff --git a/books/bookvol5.pamphlet b/books/bookvol5.pamphlet
index 8ad8238..8d8276f 100644
--- a/books/bookvol5.pamphlet
+++ b/books/bookvol5.pamphlet
@@ -61470,16 +61470,39 @@ There are 8 parts of an htPage:
 \end{chunk}
 
 \chapter{Utility functions}
+\section{Utility functions}
 
 \defun{readline}{readline}
 \begin{chunk}{defun readline}
-(DEFUN READLINE (t1)
+(defun readline (t1)
  (if t1
   (|read-line| t1)
   (|read-line| *STANDARD-INPUT*)))
 
 \end{chunk}
 
+\defun{isWrapped}{isWrapped}
+This was proven by ACL2 to accept any input and return either T or NIL.
+Note that ACL2 does not support FLOATP.
+\begin{verbatim}
+(defun isWrapped (x)
+  (or (and (consp x) (eq (car x) 'wrapped)) 
+      (acl2-numberp x)
+      (stringp x)))
+==>
+(OR (EQUAL (ISWRAPPED X) T) (EQUAL (ISWRAPPED X) NIL))
+
+\end{verbatim}
+\sig{isWrapped}{t}{(or t nil)}
+\begin{chunk}{defun isWrapped :proven}
+(defun |isWrapped| (x)
+  (or (and (consp x) (eq (qcar x) 'wrapped)) 
+      (numberp x)
+      (floatp x) 
+      (stringp x)))
+
+\end{chunk}
+
 \chapter{The Interpreter}
 \begin{chunk}{Interpreter}
 (setq *print-array* nil)
@@ -61738,6 +61761,7 @@ There are 8 parts of an htPage:
 \getchunk{defun integer-decode-float-numerator 0}
 \getchunk{defun intloopPrefix? 0}
 \getchunk{defun isIntegerString 0}
+\getchunk{defun isWrapped :proven} 
 
 \getchunk{defun keyword 0}
 \getchunk{defun keyword? 0}
diff --git a/changelog b/changelog
index f706121..d151468 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+20150715 tpd src/axiom-website/patches.html 20150715.01.tpd.patch 
+20150715 tpd src/interp/i-util merge isWrapped function into bookvol5
+20150715 tpd books/bookvol5: Use ACL2 to prove isWrapped function
 20150711 tpd src/axiom-website/patches.html 20150711.05.tpd.patch 
 20150711 tpd src/interp/i-coerce.lisp fix use of eqType assignment
 20150711 tpd src/axiom-website/patches.html 20150711.04.tpd.patch 
diff --git a/patch b/patch
index 26d21a0..5d558f9 100644
--- a/patch
+++ b/patch
@@ -1,7 +1,11 @@
-src/interp/i-coerce.lisp fix use of eqType assignment
+books/bookvol5: Use ACL2 to prove isWrapped function
 
-Goal: Clean code
+Goal: Prove Axiom correct
 
-The eqType function disappears during compile so that 
-t := eqType t turns into t := t. The following code becomes a nop
-and has been removed.
+This is the first example of using ACL2 against the Axiom 
+common lisp code to prove the function correct. The signature
+for isWrapped is
+
+   isWrapped: t -> (or t nil)
+
+It is a predicate that takes any argument and returns either t or nil.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index d04593c..0a0ba1c 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5100,6 +5100,8 @@ books/bookvol5 merge functions used from i-coerce<br/>
 readme Add Laurent Thery to credits<br/>
 <a href="patches/20150711.05.tpd.patch">20150711.05.tpd.patch</a>
 src/interp/i-coerce.lisp fix use of eqType assignment<br/>
+<a href="patches/20150715.01.tpd.patch">20150715.01.tpd.patch</a>
+books/bookvol5: Use ACL2 to prove isWrapped function<br/>
  </body>
 </html>
 
diff --git a/src/interp/i-util.lisp.pamphlet b/src/interp/i-util.lisp.pamphlet
index 9e7b762..bec922a 100644
--- a/src/interp/i-util.lisp.pamphlet
+++ b/src/interp/i-util.lisp.pamphlet
@@ -28,12 +28,6 @@ lisp code is unwrapped.
 (DEFUN |wrap| (|x|)
   (COND ((|isWrapped| |x|) |x|) ('T (CONS 'WRAPPED |x|))))
 
-;isWrapped x == x is ['WRAPPED,:.] or NUMBERP x or FLOATP x or CVECP x
-
-(DEFUN |isWrapped| (|x|)
-  (OR (AND (CONSP |x|) (EQ (QCAR |x|) 'WRAPPED)) (NUMBERP |x|)
-      (FLOATP |x|) (stringp |x|)))
-
 ;unwrap x ==
 ;  NUMBERP x or FLOATP x or CVECP x => x
 ;  x is ["WRAPPED",:y] => y
-- 
1.7.5.4