3
(set-enforce-redundancy t)
5
(local (include-book "../support/util"))
7
;;These macros facilitate localization of events:
9
(defmacro local-defun (&rest body)
10
(list 'local (cons 'defun body)))
12
(defmacro local-defund (&rest body)
13
(list 'local (cons 'defund body)))
15
(defmacro local-defthm (&rest body)
16
(list 'local (cons 'defthm body)))
18
(defmacro local-defthmd (&rest body)
19
(list 'local (cons 'defthmd body)))
21
(defmacro local-in-theory (&rest body)
23
(cons (cons 'in-theory (append body 'nil))
26
(defmacro defbvecp (name formals width &key thm-name hyp hints)
29
(intern-in-package-of-symbol
36
(x (cons name formals))
37
(typed-term (if (consp width)
40
(bvecp-concl (if (consp width)
41
(list 'bv-arrp x (car (last width)))
42
(list 'bvecp x width)))
44
(list 'integerp typed-term)
45
(list '<= 0 typed-term))))
46
(list* 'defthm thm-name
48
(list 'implies hyp bvecp-concl)
53
(list :forward-chaining :trigger-terms (list x))
54
(list :type-prescription
57
(list 'implies hyp concl)
59
:typed-term typed-term
60
;; hints for the corollary
66
bv-arrp-implies-nonnegative-integerp)))
70
(if hints (list :hints hints) nil))))
72
(defun sub1-induction (n)
75
(sub1-induction (1- n))))
77
; These will be the functions to disable in acl2 proofs about signal bodies.
78
; We use this in the compiler.
79
;BOZO This doesn't include cons, which can now appear in signals defs. I think that's okay, right? think
80
;about this and remove the BOZO
81
(defconst *rtl-operators-after-macro-expansion*
84
comp2< comp2<= comp2> comp2>=
86
logand1 logior1 logxor1
89
bits bitn setbits setbitn
91
* + ; from macroexpansion of mod* or mod+
93
floor rem decode encode
94
;; bind ; handled specially in fixup-term
95
;; if1 ; a macro, so we don't disable it
96
;; quote, n!, arr0 ; handled specially in fixup-term
97
natp1 ; doesn't matter, only occurs in for-loop defuns (must be enabled in those proofs anyway)
101
; Macro fast-and puts conjunctions in a tree form, which can avoid stack
102
; overflows by ACL2's translate functions.
104
(defun split-list (lst lo hi)
108
(mv (cons (car lst) lo) hi))
110
(split-list (cddr lst)
112
(cons (cadr lst) hi)))))
114
(defun fast-and-fn (conjuncts)
115
(declare (xargs :mode :program))
116
(cond ((endp conjuncts) ''t)
117
((endp (cdr conjuncts)) (car conjuncts))
120
(split-list conjuncts () ())
126
(defmacro fast-and (&rest conjuncts)
127
(fast-and-fn conjuncts))