File: sum-list-example.lisp

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (87 lines) | stat: -rw-r--r-- 3,302 bytes parent folder | download | duplicates (4)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
; This file illustrates Version 1.8 as of Nov 2, 1994.  We start in
; the default :logic mode with guard checking on, i.e. ,the prompt
; is ACL2 !>.

(defun sum-list (x)
  (declare (xargs :guard (integer-listp x) :verify-guards nil))
  (cond ((endp x) 0)
        (t (+ (car x) (sum-list (cdr x))))))

; Note that we disable guard verification above.  We can now evaluate
; calls of this function.  

(sum-list '(1 2 3 4))   ; this call succeeds.

(sum-list '(1 2 abc 3 4 . xyz))  ; this one fails because of a guard violation.

; It is surprising, perhaps, to note that the violation is on the guard of
; endp, not the guard of sum-list.  Because we have not yet verified the guards
; of sum-list we only have a logical definition.  But because endp has had its
; guards verified, we can run either the Common Lisp or the logical version of
; it and with guard checking on we are running the Common Lisp one.
; So we switch to no guard checking...

:set-guard-checking nil

(sum-list '(1 2 abc 3 4 . xyz))  ; Now this call succeeds.

; We prove an important theorem about sum-list.  Note that we do not have
; to restrict it with any hypotheses.

(defthm sum-list-append
  (equal (sum-list (append a b))
         (+ (sum-list a) (sum-list b))))

; Ok, we now move on to the task of showing these results hold in Common Lisp.

(verify-guards sum-list)  ; this is just like it was in Version 1.7

:comp sum-list            ; this compiles both the Common Lisp version of
                          ; sum-list and the logical (Nqthm-like ``*1*'') 
                          ; version
; Now we exit the loop and install a trace on the Common Lisp program 
; sum-list, and then reenter the loop.

:q
(trace sum-list)
(lp)

; Recall that guard checking is still off.  The following call violates the
; guards of sum-list, but since guard checking is off, we get the logical
; answer.  It is done without running the Common Lisp version of sum-list.
; That is, no trace output is evident.

(sum-list '(1 2 abc 3 4))  ; succeeds (but runs the compiled *1* function)

; But the following call prints a lot of trace output.  Because the
; guard is satisfied and we can run sum-list directly in Common Lisp.

(sum-list '(1 2 3 4))      ; succeeds (running compiled sum-list)

; Next we turn our attention to verifying that sum-list-append
; holds in Common Lisp.  If we try

(verify-guards sum-list-append)

; it fails.  Among other things, the guard for append is violated since we know
; nothing about a.  We need a version of the theorem with some hypotheses
; restricting the variables.  We state the theorem with IF so that the
; hypotheses govern the conclusion.  (At the moment in Version 1.8 IMPLIES is a
; function, not a macro, and hence in (IMPLIES p q), q is not governed by p.)

(defthm common-lisp-version-of-sum-list-append
  (if (and (integer-listp a)
           (integer-listp b))
      (= (sum-list (append a b))
         (+ (sum-list a) (sum-list b)))
      t)
  :rule-classes nil)

; The theorem above is trivially proved, because its conclusion is true
; without the hypotheses.  But we can now verify that its guards hold.

(verify-guards common-lisp-version-of-sum-list-append)

; So that expression will all evaluate to non-nil without error in
; Common Lisp (except for resource errors).