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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
|
#|
Some utility functions built on top of the ACL2s interface.
|#
(in-package "ACL2S-INTERFACE-EXTRAS")
;;;; Error conditions
(define-condition acl2s-interface-error (error)
((desc :initarg :desc :reader acl2s-interface-error/desc)
(query :initarg :query :reader acl2s-interface-error/query)
(err :initarg :err :reader acl2s-interface-error/err))
(:report
(lambda (condition stream)
(format
stream
"Error occurred when running acl2s interface call:~% error ~a ~% for query: ~a ~% ~S"
(acl2s-interface-error/err condition)
(acl2s-interface-error/query condition)
(acl2s-interface-error/desc condition)))))
(define-condition unexpected-response-error (error)
((desc :initarg :desc :reader unexpected-response-error/desc)
(query :initarg :query :reader unexpected-response-error/query)
(res :initarg :res :reader unexpected-response-error/res))
(:report
(lambda (condition stream)
(format
stream
"Unexpected response from acl2s interface call:~% error ~a ~% for query: ~a ~% ~S"
(unexpected-response-error/res condition)
(unexpected-response-error/query condition)
(unexpected-response-error/desc condition)))))
;;;; Utilities for dealing with propositional expressions
(defun replace-in (x to-replace replace-with)
"Replace to-replace with replace-with inside of x, recursively if x is a cons.
Uses 'equal to compare elements with to-replace."
(cond ((equal x to-replace) replace-with)
((consp x) (cons
(replace-in (car x) to-replace replace-with)
(replace-in (cdr x) to-replace replace-with)))
(t x)))
(defun flatten-and-step (fs)
"Given a list of statements, expand any conjunctions."
(cond ((endp fs) nil)
((or (equal 'and (caar fs)) (equal '^ (caar fs))) ;; support ACL2s ^ in addition to and
(append (cdar fs) (flatten-and-step (cdr fs))))
(t (cons (car fs) (flatten-and-step (cdr fs))))))
;; (assert (equal (flatten-and-step '(a b (and c d) (and e (and f g)))) '(a b c d e (and f g))))
;; (assert (equal (flatten-and-step '(a (^ b (and c d)) (and (^ e f) g))) '(a b (and c d) (^ e f) g)))
(defun flatten-and (fs &optional (ls nil))
"Given a list of terms representing the conjunction of those terms,
flatten any 'ands inside those terms and simplify."
(if (equal fs ls)
fs
(flatten-and (flatten-and-step fs) fs)))
;; (assert (equal (flatten-and '(a b (and c d) (and e (and f g)))) '(a b c d e f g)))
;; (assert (equal (flatten-and '(a (^ b (and c d)) (and (^ e f) g))) '(a b c d e f g)))
(defun conjunction-terms (t1 t2)
"Given two terms, produce the conjunction of them, simplifying if
either of the terms has a top-level and."
(let* ((t1-terms (if (or (equal (car t1) 'and) (equal (car t1) '^)) (cdr t1) (list t1)))
(t2-terms (if (or (equal (car t2) 'and) (equal (car t2) '^)) (cdr t2) (list t2)))
(terms (append t1-terms t2-terms))
(flat-terms (remove-duplicates (flatten-and terms) :test #'equal)))
`(and ,@flat-terms)))
;; (assert (equal (conjunction-terms 'x 'y) '(and x y)))
;; (assert (equal (conjunction-terms '(and a b) '(^ c d)) '(and a b c d)))
(defun cnf-disjunct-to-or (expr)
"Given a CNF disjunct, convert to an equivalent ACL2s expression."
(if (and (consp expr) (endp (cdr expr)))
(car expr)
(cons 'or expr)))
;; (assert (equal (cnf-disjunct-to-or '(x)) 'x))
;; (assert (equal (cnf-disjunct-to-or '(x y)) '(or x y)))
(defun conjunction-to-list (term)
"Convert a term to a list of conjuncts.
If the term is an and, this will return a list containing the arguments to that and.
Otherwise a list containing only the given term is returned."
(if (and (consp term) (equal 'and (car term)))
(cdr term)
(list term)))
(defun get-hyps (expr)
"Get the hypotheses of an implication, returning nil if the given expression
is not an implication"
(if (and (consp expr) (equal (car expr) 'implies))
(conjunction-to-list (second expr))
nil))
(assert (equal (get-hyps '(implies (and x y) z)) '(x y)))
(assert (equal (get-hyps '(and x y)) nil))
(assert (equal (get-hyps '(implies (and x y (and z w)) q)) '(x y (and z w))))
(defun get-conc (expr)
"Get the conclusion of an implication, returning nil if the given expression
is not an implication"
(if (and (consp expr) (equal (car expr) 'implies))
(third expr)
nil))
(assert (equal (get-conc '(implies (and x y) z)) 'z))
(assert (equal (get-conc '(and x y)) nil))
(assert (equal (get-conc '(implies (and x y) (implies (and z w) q))) '(implies (and z w) q)))
(defun acl2s-query-error? (res)
(car res))
(defun thm-query-error? (res)
(car res))
;; Run a thm on the given statement.
(defun acl2s-thm (q &optional goal-hints)
(acl2s-query
`(thm ,q :hints (("Goal" ,@goal-hints)))))
;; A call to guard-obligation inside of an acl2s-query should return something of the form:
;; ('ctx error-message) if guard-obligation had an internal error
;; (i.e. if the expression whose guard obligations are being asked for contains an undefined function)
;; or
;; (nil (term-info obligations)) otherwise
;; where term-info is of the form (:term ...)
;; and obligations is a list of obligations
(defun guard-obligations-query-res-ok? (res)
"Determine if `res` is of a form that we expect guard-obligation to return."
(and (consp res)
(>= (length res) 2)
(consp (second res))
(>= (length (second res)) 2)))
(defun guard-obligations-query (expr &key (debug nil) (simplify t))
"Get the guard obligations for the given expression, possibly with debug info (depending on debug argument)
This will return a CNF of the guard obligations
This will error if the internal acl2s-query returns an unexpected value, or if an error is detected"
(let ((res (acl2s-query `(mv-let
(erp val)
(guard-obligation ',expr nil ,debug ,simplify 'ctx state)
(mv erp val state)))))
(cond ((not (guard-obligations-query-res-ok? res))
(error "acl2s-query returned an unexpected response in guard-obligations-query: ~a" res))
((or (car res) (equal (car res) 'ctx))
(error "Error when computing guard obligations for the expression ~S:~%~S" expr res))
(t (second (second res))))))
;;(assert (equal (guard-obligations-query '(app x nil)) '(((true-listp x)))))
(defun rguard-obligations-debug (expr &key (simplify t))
"Get the guard obligations of the given expression.
This returns a list containing lists where:
- the first element is the debug info (describing where the obligation came from).
- the second element is a statement describing the obligation itself.
Obligations are converted to ors here so that they can be directly run in ACL2.
ACL2-numberp is replaced by rationalp inside of obligations."
(let ((val (guard-obligations-query expr :debug t :simplify simplify)))
(mapcar (lambda (x)
(list (second (car x))
(replace-in (cnf-disjunct-to-or (cdr x))
'acl2-numberp
'rationalp)))
val)))
;;(assert (equal (rguard-obligations-debug '(app x nil))
;; '(((extra-info ':top-level '(app x nil)) (true-listp x)))))
(defun rguard-obligations (expr &key (simplify t))
"Get the guard obligations of the given expression.
This returns a list containing statements describing the obligations themselves.
Obligations are converted to ors here so that they can be directly run in ACL2.
ACL2-numberp is replaced by rationalp inside of obligations."
(let ((val (guard-obligations-query expr :debug nil :simplify simplify)))
(mapcar (lambda (x) (replace-in (cnf-disjunct-to-or x)
'acl2-numberp
'rationalp))
val)))
;;(assert (equal (rguard-obligations '(app x nil)) '(true-listp x)))
;;(assert (equal (rguard-obligations '(app x nil) :simplify nil) '((true-listp x) (true-listp 'nil))))
(defun acl2s-untranslate (x)
"Untranslate an expression."
(cadr (acl2s-query
`(mv nil
(untranslate ',x nil (w state))
state))))
;;(assert (equal (acl2s-untranslate '(BINARY-+ '1 (BINARY-+ '2 '3))) '(+ 1 2 3)))
(defun reset-file ()
"Reset the ACL2 state back to before the definition of START-LOAD-FILE"
(acl2::ld '(:ubt START-LOAD-FILE)))
(defun create-reset-point ()
"Define a function so that one can undo back to this point in the ACL2 world."
;; Create this function so that we can come back to this point in ACL2's history
(acl2s-event '(defun START-LOAD-FILE () t)))
(defun acl2s-arity (f)
"A function that determines if f is a function defined in ACL2s and if
so, produces its arity (number of arguments). If f is not a function, then
the arity is nil. Otherwise, the arity is a natural number. Note that f
can't be a macro."
(second (acl2s-compute `(acl2::arity ',f (w state)))))
;;(assert (equal (acl2s-arity 'append) nil)) ;; is nil since append is a macro
;;(assert (equal (acl2s-arity 'binary-append) 2))
(declaim (ftype (function (symbol) boolean) is-theorem?))
(defun is-theorem? (sym)
"Determine if the given symbol symbol names a theorem."
(let* ((query `(acl2::theorem-namep ',sym (w state)))
(res (acl2s-compute query)))
(if (acl2s-query-error? res)
(error (format nil "Internal acl2s query error for query ~a" query))
(second res))))
|
