← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/misc/bash.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/misc/bash.lisp
 
1
; Copyright (C) 2006  University of Texas at Austin
 
2
 
 
3
; This program is free software; you can redistribute it and/or modify
 
4
; it under the terms of the GNU General Public License as published by
 
5
; the Free Software Foundation; either version 2 of the License, or
 
6
; (at your option) any later version.
 
7
 
 
8
; This program is distributed in the hope that it will be useful,
 
9
; but WITHOUT ANY WARRANTY; without even the implied warranty of
 
10
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
11
; GNU General Public License for more details.
 
12
 
 
13
; You should have received a copy of the GNU General Public License
 
14
; along with this program; if not, write to the Free Software
 
15
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
16
 
 
17
; Written by:  Matt Kaufmann
 
18
; email:       Kaufmann@cs.utexas.edu
 
19
; Department of Computer Sciences
 
20
; University of Texas at Austin
 
21
; Austin, TX 78712-1188 U.S.A.
 
22
 
 
23
; October, 2006
 
24
 
 
25
; In a nutshell:
 
26
 
 
27
; If you submit (bash term), then the result is a list of goals to which ACL2
 
28
; can simplify term when attempting to prove it.  (In particular, if the result
 
29
; is nil, then ACL2 can prove term.)  More accurately: (bash term) returns (mv
 
30
; erp val state), where: erp is nil unless there is an error; and val is a list
 
31
; of terms, in untranslated (user-level) form, whose provability implies the
 
32
; provability of the input term.  If ACL2 cannot simplify the input term, then
 
33
; there is an error, i.e., erp is not nil.
 
34
 
 
35
; More details:
 
36
 
 
37
; This book defines a utility similar to the proof-checker's bash command, but
 
38
; for use in the top-level loop.  The input term can be a user-level term,
 
39
; i.e., it need not be translated.  Thus this bash utility is given a term, and
 
40
; it returns an error triple (mv erp termlist state) where if erp is not nil,
 
41
; then termlist is the list of goals that ACL2 would get stuck on, if you were
 
42
; to attempt to prove the given term with only simplification, i.e., with a
 
43
; "Goal" hint of :do-not '(generalize eliminate-destructors fertilize
 
44
; eliminate-irrelevance) and with induction turned off.  Bash does all the
 
45
; normal simplification stuff, including forward chaining.  Use :hints to
 
46
; specify hints using the same syntax as for thm and defthm.  Use a non-nil
 
47
; value of :verbose if you want output, including the proof attempt.  The
 
48
; keyword values are not evaluated, so :hints could be of the form (("Goal
 
49
; ...)) but not '(("Goal" ...)).
 
50
 
 
51
; This book also includes a functional (non-macro) version of bash, bash-fn.
 
52
; At the end is a variant contributed by Dave Greve, bash-term-to-dnf, that
 
53
; returns a list of goals (implicitly conjoined) where each goal has the form
 
54
; (lit1 lit2 ... litk), for which the goal is equivalent to the negation of the
 
55
; conjunction of the liti.
 
56
 
 
57
; Examples:
 
58
 
 
59
#|
 
60
ACL2 !>(bash (equal (append x y) (append (car (cons x a)) z)))
 
61
 ((EQUAL (APPEND X Y) (APPEND X Z)))
 
62
ACL2 !>(bash (equal (car (cons x y)) x))
 
63
 NIL
 
64
ACL2 !>(bash (implies (true-listp x) (equal (append x y) zzz))
 
65
             :hints (("Goal" :expand ((true-listp x)
 
66
                                      (true-listp (cdr x))
 
67
                                      (append x y)))))
 
68
 ((EQUAL Y ZZZ)
 
69
  (IMPLIES (AND (CONSP X)
 
70
                (CONSP (CDR X))
 
71
                (TRUE-LISTP (CDDR X)))
 
72
           (EQUAL (LIST* (CAR X)
 
73
                         (CADR X)
 
74
                         (APPEND (CDDR X) Y))
 
75
                  ZZZ))
 
76
  (IMPLIES (AND (CONSP X) (NOT (CDR X)))
 
77
           (EQUAL (CONS (CAR X) Y) ZZZ)))
 
78
ACL2 !>(bash-term-to-dnf
 
79
        '(implies (true-listp x) (equal (append x y) zzz))
 
80
        '(("Goal" :expand ((true-listp x)
 
81
                           (true-listp (cdr x))
 
82
                           (append x y))))
 
83
        nil state)
 
84
 (((EQUAL Y ZZZ))
 
85
  ((NOT (CONSP X))
 
86
   (NOT (CONSP (CDR X)))
 
87
   (NOT (TRUE-LISTP (CDDR X)))
 
88
   (EQUAL (LIST* (CAR X)
 
89
                 (CADR X)
 
90
                 (APPEND (CDDR X) Y))
 
91
          ZZZ))
 
92
  ((NOT (CONSP X))
 
93
   (CDR X)
 
94
   (EQUAL (CONS (CAR X) Y) ZZZ)))
 
95
ACL2 !>
 
96
|# ; |
 
97
 
 
98
(in-package "ACL2")
 
99
 
 
100
(program)
 
101
 
 
102
(set-state-ok t)
 
103
 
 
104
(defun simplify-with-prover (form hints ctx state)
 
105
 
 
106
; This is patterned after (define-pc-primitive prove ...).
 
107
 
 
108
  (let ((wrld (w state))
 
109
        (ens (ens state))
 
110
        (name-tree 'bash))
 
111
    (er-let*
 
112
     ((thints (translate-hints
 
113
               name-tree
 
114
 
 
115
; Keep the following in sync with the definition of the proof-checker :bash
 
116
; command.
 
117
 
 
118
               (append
 
119
                *bash-skip-forcing-round-hints*
 
120
                (add-string-val-pair-to-string-val-alist
 
121
                 "Goal"
 
122
                 :do-not
 
123
                 (list 'quote '(generalize eliminate-destructors fertilize
 
124
                                           eliminate-irrelevance))
 
125
                 (add-string-val-pair-to-string-val-alist
 
126
                  "Goal"
 
127
                  :do-not-induct
 
128
                  name-tree
 
129
                  hints))
 
130
                (default-hints wrld))
 
131
               ctx wrld state))
 
132
      (tterm (translate form t t t ctx wrld state)))
 
133
     (mv-let (erp ttree state)
 
134
             (pc-prove tterm form thints t ens wrld ctx state)
 
135
             (cond (erp (mv t nil state))
 
136
                   (t (let ((clauses (unproved-pc-prove-terms ttree)))
 
137
                        (cond ((and (eql (length clauses) 1)
 
138
                                    (eql (length (car clauses)) 1)
 
139
                                    (eql (caar clauses) tterm))
 
140
                               (mv 'no-change nil state))
 
141
                              (t (value clauses))))))))))
 
142
 
 
143
(defun bash-fn (form hints verbose ctx state)
 
144
 
 
145
; Keep this in sync with bash-term-to-dnf.
 
146
 
 
147
  (mv-let
 
148
   (erp clauses state)
 
149
   (cond (verbose
 
150
          (simplify-with-prover form hints ctx state))
 
151
         (t
 
152
          (state-global-let*
 
153
           ((inhibit-output-lst *valid-output-names*))
 
154
           (simplify-with-prover form hints ctx state))))
 
155
   (cond
 
156
    (erp
 
157
     (pprogn
 
158
      (warning$ ctx "bash"
 
159
                "Unable to simplify the input term~@0"
 
160
                (cond ((eq erp 'no-change)
 
161
                       ".")
 
162
                      (t (msg " because an error occurred.~@0"
 
163
                              (cond
 
164
                               (verbose "")
 
165
                               (t "  Try setting the verbose flag to t in ~
 
166
                                    order to see what is going on."))))))
 
167
      (value (list form))))
 
168
    (t
 
169
     (value (prettyify-clause-lst clauses (let*-abstractionp state) (w state)))))))
 
170
 
 
171
(defmacro bash (term &key verbose hints)
 
172
  `(bash-fn ',term ',hints ',verbose 'bash state))
 
173
 
 
174
; Dave Greve has contributed the following (only slightly modified here), to
 
175
; create a variant bash-term-to-dnf of bash-fn.  This example may suggest other
 
176
; variants; feel free to contribute yours to Matt Kaufmann,
 
177
; kaufmann@cs.utexas.edu.
 
178
 
 
179
(defun goals-to-cnf (goals)
 
180
  (cond ((endp goals) nil)
 
181
        (t (cons (append (access goal (car goals) :hyps)
 
182
                         (list (dumb-negate-lit (access goal (car goals)
 
183
                                                        :conc))))
 
184
                 (goals-to-cnf (cdr goals))))))
 
185
 
 
186
(defun untranslate-lst-lst (list iff-flg wrld)
 
187
  (cond
 
188
   ((endp list)
 
189
    nil)
 
190
   (t (cons (untranslate-lst (car list) iff-flg wrld)
 
191
            (untranslate-lst-lst (cdr list) iff-flg wrld)))))
 
192
 
 
193
(defun bash-term-to-dnf (form hints verbose state)
 
194
 
 
195
; Keep this in sync with bash-fn.
 
196
 
 
197
  (let ((ctx 'bash-term-to-dnf))
 
198
    (mv-let
 
199
     (erp clauses state)
 
200
     (cond (verbose
 
201
            (simplify-with-prover form hints ctx state))
 
202
           (t
 
203
            (state-global-let*
 
204
             ((inhibit-output-lst *valid-output-names*))
 
205
             (simplify-with-prover form hints ctx state))))
 
206
     (cond
 
207
      (erp
 
208
       (pprogn
 
209
        (warning$ ctx "bash"
 
210
                  "Unable to simplify the input term~@0"
 
211
                  (cond ((eq erp 'no-change)
 
212
                         ".")
 
213
                        (t (msg " because an error occurred.~@0"
 
214
                                (cond
 
215
                                 (verbose "")
 
216
                                 (t "  Try setting the verbose flag to t in ~
 
217
                                     order to see what is going on."))))))
 
218
        (value (list (list form)))))
 
219
      (t
 
220
       (value (untranslate-lst-lst clauses t (w state))))))))