← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/lib/util.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/rtl/rel6/lib/util.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(set-enforce-redundancy t)
 
4
 
 
5
(local (include-book "../support/top/top"))
 
6
 
 
7
;;These macros facilitate localization of events:
 
8
 
 
9
(defmacro local-defun (&rest body)
 
10
  (list 'local (cons 'defun body)))
 
11
 
 
12
(defmacro local-defund (&rest body)
 
13
  (list 'local (cons 'defund body)))
 
14
 
 
15
(defmacro local-defthm (&rest body)
 
16
  (list 'local (cons 'defthm body)))
 
17
 
 
18
(defmacro local-defthmd (&rest body)
 
19
  (list 'local (cons 'defthmd body)))
 
20
 
 
21
(defmacro local-in-theory (&rest body)
 
22
  (cons 'local
 
23
        (cons (cons 'in-theory (append body 'nil))
 
24
              'nil)))
 
25
 
 
26
(defmacro defbvecp (name formals width &key thm-name hyp hints)
 
27
  (let* ((thm-name
 
28
          (or thm-name
 
29
              (intern-in-package-of-symbol
 
30
               (concatenate 'string
 
31
                            (if (consp width)
 
32
                                "BV-ARRP$"
 
33
                              "BVECP$")
 
34
                            (symbol-name name))
 
35
               name)))
 
36
         (x (cons name formals))
 
37
         (typed-term (if (consp width)
 
38
                         (list 'ag 'index x)
 
39
                       x))
 
40
         (bvecp-concl (if (consp width)
 
41
                          (list 'bv-arrp x (car (last width)))
 
42
                        (list 'bvecp x width)))
 
43
         (concl (list 'and
 
44
                      (list 'integerp typed-term)
 
45
                      (list '<= 0 typed-term))))
 
46
    (list* 'defthm thm-name
 
47
           (if hyp
 
48
               (list 'implies hyp bvecp-concl)
 
49
             bvecp-concl)
 
50
           :rule-classes
 
51
           (list
 
52
            :rewrite
 
53
            (list :forward-chaining :trigger-terms (list x))
 
54
            (list :type-prescription
 
55
                  :corollary
 
56
                  (if hyp
 
57
                      (list 'implies hyp concl)
 
58
                    concl)
 
59
                  :typed-term typed-term
 
60
                  ;; hints for the corollary 
 
61
                  :hints
 
62
                  (if (consp width)
 
63
                      '(("Goal"
 
64
                         :in-theory
 
65
                         '(implies bvecp
 
66
                                   bv-arrp-implies-nonnegative-integerp)))
 
67
                    '(("Goal"
 
68
                       :in-theory
 
69
                       '(implies bvecp))))))
 
70
           (if hints (list :hints hints) nil))))
 
71
 
 
72
(defun sub1-induction (n)
 
73
      (if (zp n)
 
74
          n
 
75
        (sub1-induction (1- n))))
 
76
 
 
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*
 
82
  '(log= log<> 
 
83
    log< log<= log> log>= 
 
84
    comp2< comp2<= comp2> comp2>=
 
85
    land lior lxor lnot
 
86
    logand1 logior1 logxor1
 
87
    shft
 
88
    cat mulcat
 
89
    bits bitn setbits setbitn 
 
90
    ag as
 
91
    * + ; from macroexpansion of mod* or mod+
 
92
    ;mod- ;now a macro!
 
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)
 
98
    mk-bvarr mk-bvec
 
99
    ))
 
100
 
 
101
; Macro fast-and puts conjunctions in a tree form, which can avoid stack
 
102
; overflows by ACL2's translate functions.
 
103
 
 
104
(defun split-list (lst lo hi)
 
105
  (cond ((endp lst) 
 
106
         (mv lo hi))
 
107
        ((endp (cdr lst)) 
 
108
         (mv (cons (car lst) lo) hi))
 
109
        (t
 
110
         (split-list (cddr lst)
 
111
                     (cons (car lst) lo)
 
112
                     (cons (cadr lst) hi)))))
 
113
 
 
114
(defun fast-and-fn (conjuncts)
 
115
  (declare (xargs :mode :program))
 
116
  (cond ((endp conjuncts) ''t)
 
117
        ((endp (cdr conjuncts)) (car conjuncts))
 
118
        (t
 
119
         (mv-let (hi lo)
 
120
             (split-list conjuncts () ())
 
121
           (list 'if
 
122
                 (fast-and-fn hi)
 
123
                 (fast-and-fn lo)
 
124
                 'nil)))))
 
125
 
 
126
(defmacro fast-and (&rest conjuncts)
 
127
  (fast-and-fn conjuncts))