← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/mlib/namemangle.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/namemangle.lisp
95
95
             (len gateinsts)))))
96
96
 
97
97
 
98
 
(define vl-namemangle-netdecls
99
 
  :short "Safely try to give these netdecls new names of the form
 
98
(define vl-namemangle-vardecls
 
99
  :short "Safely try to give these vardecls new names of the form
100
100
@('prefix_{current-name}.')"
101
101
 
102
102
  ((prefix   stringp)
103
 
   (netdecls vl-netdecllist-p)
 
103
   (vardecls vl-vardecllist-p)
104
104
   (nf       vl-namefactory-p))
105
 
  :returns (mv (new-nets vl-netdecllist-p)
 
105
  :returns (mv (new-vars vl-vardecllist-p)
106
106
               (new-nf   vl-namefactory-p))
107
107
 
108
108
  :long "<p>You'll generally want to do something like:</p>
109
109
 
110
110
@({
111
 
   (pairlis$ (vl-netdecllist->names old-netdecls)
112
 
             (vl-netdecllist->names renamed-netdecls))
 
111
   (pairlis$ (vl-vardecllist->names old-vardecls)
 
112
             (vl-vardecllist->names renamed-vardecls))
113
113
})
114
114
 
115
115
<p>And then use this as a substitution.</p>"
116
116
 
117
 
  (b* (((when (atom netdecls))
 
117
  (b* (((when (atom vardecls))
118
118
        (mv nil (vl-namefactory-fix nf)))
119
 
       (name1          (vl-netdecl->name (car netdecls)))
 
119
       (name1          (vl-vardecl->name (car vardecls)))
120
120
       (want1          (str::cat prefix "_" name1))
121
121
       ((mv fresh1 nf) (vl-namefactory-plain-name want1 nf))
122
 
       (inst1          (change-vl-netdecl (car netdecls) :name fresh1))
123
 
       ((mv insts2 nf) (vl-namemangle-netdecls prefix (cdr netdecls) nf)))
 
122
       (inst1          (change-vl-vardecl (car vardecls) :name fresh1))
 
123
       ((mv insts2 nf) (vl-namemangle-vardecls prefix (cdr vardecls) nf)))
124
124
    (mv (cons inst1 insts2) nf))
125
125
  ///
126
 
  (defmvtypes vl-namemangle-netdecls (true-listp nil))
 
126
  (defmvtypes vl-namemangle-vardecls (true-listp nil))
127
127
 
128
 
  (defthm len-of-vl-namemangle-netdecls
129
 
    (b* (((mv new-netdecls ?new-nf)
130
 
          (vl-namemangle-netdecls loc netdecls nf)))
131
 
      (equal (len new-netdecls)
132
 
             (len netdecls)))))
 
128
  (defthm len-of-vl-namemangle-vardecls
 
129
    (b* (((mv new-vardecls ?new-nf)
 
130
          (vl-namemangle-vardecls loc vardecls nf)))
 
131
      (equal (len new-vardecls)
 
132
             (len vardecls)))))
133
133