← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/loader/config.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/loader/config.lisp
30
30
 
31
31
(in-package "VL")
32
32
(include-book "preprocessor/defines")
 
33
(local (include-book "../util/arithmetic"))
 
34
(local (include-book "../util/osets"))
 
35
 
 
36
(local (defthm string-listp-of-remove-equal
 
37
         (implies (force (string-listp x))
 
38
                  (string-listp (remove-equal a x)))))
 
39
 
 
40
(local (defthm string-listp-of-remove-duplicates-equal
 
41
         (implies (force (string-listp x))
 
42
                  (string-listp (remove-duplicates-equal x)))))
33
43
 
34
44
(define mintime-p (x)
35
45
  (or (not x)
96
106
   (search-path    string-listp
97
107
                   "A list of directories to search (in order) for descriptions
98
108
                    in @('start-modnames') that were in the @('start-files'),
99
 
                    and for <see topic=\"@(url vl-modulelist-missing)\">missing
100
 
                    modules</see>.  This is similar to \"library directories\"
101
 
                    in tools like Verilog-XL and NCVerilog.")
 
109
                    and for missing modules.  This is similar to \"library
 
110
                    directories\" in tools like Verilog-XL and NCVerilog.")
102
111
 
103
112
   (search-exts    string-listp
104
113
                   :default '("v")
141
150
(defconst *vl-default-loadconfig*
142
151
  (make-vl-loadconfig))
143
152
 
 
153
(local (xdoc::set-default-parents vl-loadconfig-clean))
 
154
 
 
155
 
 
156
(define vl-clean-search-extension ((searchext stringp))
 
157
  :short "Normalize search extensions so that they don't have leading dots."
 
158
  :long "<p>This is a DWIM feature so that we can just do the right thing
 
159
regardless of whether you say the search extensions are, e.g., @('\".sv\"') or
 
160
just @('\"sv\"').</p>"
 
161
  :returns (new-searchext stringp :rule-classes :type-prescription)
 
162
  (b* ((searchext (string-fix searchext))
 
163
       (len (length searchext))
 
164
       ((when (and (< 0 len)
 
165
                   (eql (char searchext 0) #\.)))
 
166
        (subseq searchext 1 nil)))
 
167
    searchext)
 
168
  ///
 
169
  (assert! (equal (vl-clean-search-extension "sv") "sv"))
 
170
  (assert! (equal (vl-clean-search-extension ".sv") "sv")))
 
171
 
 
172
(defprojection vl-clean-search-extensions-aux ((x string-listp))
 
173
  :returns (new-x string-listp)
 
174
  (vl-clean-search-extension x))
 
175
 
 
176
(define vl-clean-search-extensions ((search-exts string-listp))
 
177
  :returns (search-exts string-listp)
 
178
  (remove-duplicates-equal (remove-equal "" (vl-clean-search-extensions-aux search-exts)))
 
179
  ///
 
180
  (assert! (equal (vl-clean-search-extensions '("v" "v" ".v" "sv")) '("v" "sv")))
 
181
  (assert! (equal (vl-clean-search-extensions '(".v" "v")) '("v")))
 
182
  (assert! (equal (vl-clean-search-extensions '(".sv" "v" "sv" "v")) '("sv" "v"))))
 
183
 
 
184
(define vl-loadconfig-clean
 
185
  :parents (vl-loadconfig)
 
186
  :short "Normalize a load configuration to avoid, e.g., redundant search paths
 
187
  and extensions."
 
188
  ((config vl-loadconfig-p))
 
189
  :returns (new-config vl-loadconfig-p)
 
190
  :long "<p>We clean up the load configuration in a couple of ways.  This is
 
191
partially an optimization that will help us to avoid looking in the same
 
192
directories multiple times.  It also helps to prevent spurious \"ambiguous
 
193
load\" warnings that could arise if someone gives the same search extensions
 
194
multiple times.</p>"
 
195
  (b* (((vl-loadconfig config)))
 
196
    (change-vl-loadconfig config
 
197
                          ;; Don't sort start-files in case the user wants to process
 
198
                          ;; them multiple times.
 
199
                          :start-names (mergesort config.start-names)
 
200
                          ;; We use remove-duplicates-equal instead of
 
201
                          ;; mergesort, even though it is generally slow,
 
202
                          ;; because it preserves the original order, which
 
203
                          ;; matters for priority-ordered search paths/exts.
 
204
                          :search-path (remove-duplicates-equal config.search-path)
 
205
                          :search-exts (vl-clean-search-extensions config.search-exts)
 
206
                          :include-dirs (remove-duplicates-equal config.include-dirs))))