← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/centaur/vl/mlib/context.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/centaur/vl/mlib/context.lisp
30
30
 
31
31
(in-package "VL")
32
32
(include-book "../parsetree")
33
 
(local (include-book "../util/arithmetic"))
34
 
(local (std::add-default-post-define-hook :fix))
35
 
 
36
 
(defsection context
37
 
  :parents (mlib)
38
 
  :short "Tools for working with \"arbitrary\" module elements.  These
39
 
functions are often useful, e.g., when writing linter checks, or when writing
40
 
warning messages that need to explain where an error occurs.")
41
 
 
42
 
(local (xdoc::set-default-parents context))
43
 
 
44
 
(deftranssum vl-modelement
45
 
  :short "Recognizer for an arbitrary module element."
46
 
 
47
 
  :long "<p>It is sometimes useful to be able to deal with module elements of
48
 
arbitrary types.  For instance, we often use this in error messages, along with
49
 
@(see vl-context-p), to describe where expressions occur.  We also use it in
50
 
our @(see parser), where before module formation, the module elements are
51
 
initially kept in a big, mixed list.</p>"
52
 
  (vl-port
53
 
   vl-portdecl
54
 
   vl-assign
55
 
   vl-netdecl
56
 
   vl-vardecl
57
 
   vl-paramdecl
58
 
   vl-fundecl
59
 
   vl-taskdecl
60
 
   vl-modinst
61
 
   vl-gateinst
62
 
   vl-always
63
 
   vl-initial))
64
 
 
65
 
(fty::deflist vl-modelementlist
66
 
  :elt-type vl-modelement-p)
67
 
 
68
 
(deflist vl-modelementlist-p (x)
69
 
  (vl-modelement-p x)
70
 
  :elementp-of-nil nil
71
 
  :rest
72
 
  ((defthm vl-modelementlist-p-when-vl-portlist-p
73
 
     (implies (vl-portlist-p x)
74
 
              (vl-modelementlist-p x)))
75
 
 
76
 
   (defthm vl-modelementlist-p-when-vl-portdecllist-p
77
 
     (implies (vl-portdecllist-p x)
78
 
              (vl-modelementlist-p x)))
79
 
 
80
 
   (defthm vl-modelementlist-p-when-vl-assignlist-p
81
 
     (implies (vl-assignlist-p x)
82
 
              (vl-modelementlist-p x)))
83
 
 
84
 
   (defthm vl-modelementlist-p-when-vl-netdecllist-p
85
 
     (implies (vl-netdecllist-p x)
86
 
              (vl-modelementlist-p x)))
87
 
 
88
 
   (defthm vl-modelementlist-p-when-vl-vardecllist-p
89
 
     (implies (vl-vardecllist-p x)
90
 
              (vl-modelementlist-p x)))
91
 
 
92
 
   (defthm vl-modelementlist-p-when-vl-paramdecllist-p
93
 
     (implies (vl-paramdecllist-p x)
94
 
              (vl-modelementlist-p x)))
95
 
 
96
 
   (defthm vl-modelementlist-p-when-vl-fundecllist-p
97
 
     (implies (vl-fundecllist-p x)
98
 
              (vl-modelementlist-p x)))
99
 
 
100
 
   (defthm vl-modelementlist-p-when-vl-taskdecllist-p
101
 
     (implies (vl-taskdecllist-p x)
102
 
              (vl-modelementlist-p x)))
103
 
 
104
 
   (defthm vl-modelementlist-p-when-vl-modinstlist-p
105
 
     (implies (vl-modinstlist-p x)
106
 
              (vl-modelementlist-p x)))
107
 
 
108
 
   (defthm vl-modelementlist-p-when-vl-gateinstlist-p
109
 
     (implies (vl-gateinstlist-p x)
110
 
              (vl-modelementlist-p x)))
111
 
 
112
 
   (defthm vl-modelementlist-p-when-vl-alwayslist-p
113
 
     (implies (vl-alwayslist-p x)
114
 
              (vl-modelementlist-p x)))
115
 
 
116
 
   (defthm vl-modelementlist-p-when-vl-initiallist-p
117
 
     (implies (vl-initiallist-p x)
118
 
              (vl-modelementlist-p x)))))
119
 
 
120
 
 
121
 
(define vl-modelement-loc ((x vl-modelement-p))
122
 
  :short "Get the location of any @(see vl-modelement-p)."
123
 
  :returns (loc vl-location-p
124
 
                :hints(("Goal" :in-theory (enable vl-modelement-fix))))
125
 
  (b* ((x (vl-modelement-fix x)))
126
 
    (case (tag x)
127
 
      (:vl-port      (vl-port->loc x))
128
 
      (:vl-portdecl  (vl-portdecl->loc x))
129
 
      (:vl-assign    (vl-assign->loc x))
130
 
      (:vl-netdecl   (vl-netdecl->loc x))
131
 
      (:vl-vardecl   (vl-vardecl->loc x))
132
 
      (:vl-paramdecl (vl-paramdecl->loc x))
133
 
      (:vl-fundecl   (vl-fundecl->loc x))
134
 
      (:vl-taskdecl  (vl-taskdecl->loc x))
135
 
      (:vl-modinst   (vl-modinst->loc x))
136
 
      (:vl-gateinst  (vl-gateinst->loc x))
137
 
      (:vl-always    (vl-always->loc x))
138
 
      (:vl-initial   (vl-initial->loc x)))))
139
 
 
140
 
 
141
 
 
142
 
(define vl-sort-modelements
143
 
  ((x vl-modelementlist-p)
144
 
   (ports vl-portlist-p)
145
 
   (portdecls vl-portdecllist-p)
146
 
   (assigns vl-assignlist-p)
147
 
   (netdecls vl-netdecllist-p)
148
 
   (vardecls vl-vardecllist-p)
149
 
   (paramdecls vl-paramdecllist-p)
150
 
   (fundecls vl-fundecllist-p)
151
 
   (taskdecls vl-taskdecllist-p)
152
 
   (modinsts vl-modinstlist-p)
153
 
   (gateinsts vl-gateinstlist-p)
154
 
   (alwayses vl-alwayslist-p)
155
 
   (initials vl-initiallist-p))
156
 
  :returns (mv (ports vl-portlist-p)
157
 
               (portdecls vl-portdecllist-p)
158
 
               (assigns vl-assignlist-p)
159
 
               (netdecls vl-netdecllist-p)
160
 
               (vardecls vl-vardecllist-p)
161
 
               (paramdecls vl-paramdecllist-p)
162
 
               (fundecls vl-fundecllist-p)
163
 
               (taskdecls vl-taskdecllist-p)
164
 
               (modinsts vl-modinstlist-p)
165
 
               (gateinsts vl-gateinstlist-p)
166
 
               (alwayses vl-alwayslist-p)
167
 
               (initials vl-initiallist-p))
168
 
  (b* (((when (atom x))
169
 
        (mv (rev (vl-portlist-fix ports))
170
 
            (rev (vl-portdecllist-fix portdecls))
171
 
            (rev (vl-assignlist-fix assigns))
172
 
            (rev (vl-netdecllist-fix netdecls))
173
 
            (rev (vl-vardecllist-fix vardecls))
174
 
            (rev (vl-paramdecllist-fix paramdecls))
175
 
            (rev (vl-fundecllist-fix fundecls))
176
 
            (rev (vl-taskdecllist-fix taskdecls))
177
 
            (rev (vl-modinstlist-fix modinsts))
178
 
            (rev (vl-gateinstlist-fix gateinsts))
179
 
            (rev (vl-alwayslist-fix alwayses))
180
 
            (rev (vl-initiallist-fix initials))))
181
 
       (x1  (vl-modelement-fix (car x)))
182
 
       (tag (tag x1)))
183
 
    (vl-sort-modelements (cdr x)
184
 
                         (if (eq tag :vl-port)      (cons x1 ports)      ports)
185
 
                         (if (eq tag :vl-portdecl)  (cons x1 portdecls)  portdecls)
186
 
                         (if (eq tag :vl-assign)    (cons x1 assigns)    assigns)
187
 
                         (if (eq tag :vl-netdecl)   (cons x1 netdecls)   netdecls)
188
 
                         (if (eq tag :vl-vardecl)   (cons x1 vardecls)   vardecls)
189
 
                         (if (eq tag :vl-paramdecl) (cons x1 paramdecls) paramdecls)
190
 
                         (if (eq tag :vl-fundecl)   (cons x1 fundecls)   fundecls)
191
 
                         (if (eq tag :vl-taskdecl)  (cons x1 taskdecls)  taskdecls)
192
 
                         (if (eq tag :vl-modinst)   (cons x1 modinsts)   modinsts)
193
 
                         (if (eq tag :vl-gateinst)  (cons x1 gateinsts)  gateinsts)
194
 
                         (if (eq tag :vl-always)    (cons x1 alwayses)   alwayses)
195
 
                         (if (eq tag :vl-initial)   (cons x1 initials)   initials)))
196
 
  :prepwork
197
 
  ((local (in-theory (disable
198
 
                      ;; just a speed hint
199
 
                      double-containment
200
 
                      set::nonempty-means-set
201
 
                      acl2::consp-under-iff-when-true-listp
202
 
                      acl2::consp-by-len
203
 
                      acl2::true-listp-when-character-listp
204
 
                      acl2::true-listp-when-atom
205
 
                      set::sets-are-true-lists
206
 
                      consp-when-member-equal-of-cons-listp
207
 
                      consp-when-member-equal-of-cons-listp
208
 
                      acl2::rev-when-not-consp
209
 
                      default-car
210
 
                      default-cdr
211
 
                      pick-a-point-subset-strategy
212
 
                      vl-modelement-p-when-member-equal-of-vl-modelementlist-p
213
 
                      vl-portlist-p-when-subsetp-equal
214
 
                      vl-initiallist-p-when-subsetp-equal
215
 
                      vl-assignlist-p-when-subsetp-equal
216
 
                      vl-alwayslist-p-when-subsetp-equal
217
 
                      vl-vardecllist-p-when-subsetp-equal
218
 
                      vl-paramdecllist-p-when-subsetp-equal
219
 
                      vl-netdecllist-p-when-subsetp-equal
220
 
                      vl-modinstlist-p-when-subsetp-equal
221
 
                      vl-gateinstlist-p-when-subsetp-equal
222
 
                      vl-fundecllist-p-when-subsetp-equal
223
 
                      vl-taskdecllist-p-when-subsetp-equal
224
 
                      vl-portdecllist-p-when-subsetp-equal
225
 
                      vl-modelementlist-p-when-vl-portlist-p
226
 
                      vl-modelementlist-p-when-vl-initiallist-p
227
 
                      vl-modelementlist-p-when-vl-vardecllist-p
228
 
                      vl-modelementlist-p-when-vl-portdecllist-p
229
 
                      vl-modelementlist-p-when-vl-netdecllist-p
230
 
                      vl-modelementlist-p-when-vl-modinstlist-p
231
 
                      vl-modelementlist-p-when-vl-gateinstlist-p
232
 
                      vl-modelementlist-p-when-vl-fundecllist-p
233
 
                      vl-modelementlist-p-when-vl-taskdecllist-p
234
 
                      vl-modelementlist-p-when-vl-assignlist-p
235
 
                      vl-modelementlist-p-when-vl-alwayslist-p
236
 
                      (:rules-of-class :type-prescription :here)
237
 
                      (:ruleset tag-reasoning)
238
 
                      )))))
239
 
 
240
 
(defprod vl-context
241
 
  :short "Description of where an expression occurs."
242
 
  :tag :vl-context
243
 
  :layout :tree
244
 
  ((mod  stringp :rule-classes :type-prescription
245
 
         "The module where this module element was taken from.")
246
 
   (elem vl-modelement-p
247
 
         "Some element from the module.")))
248
 
 
 
33
; cert_param: (reloc_stub)