← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/toe/toe-emodwire.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/toe/toe-emodwire.lisp
30
30
 
31
31
(in-package "VL")
32
32
(include-book "../util/defs")
 
33
(include-book "centaur/fty/deftypes" :dir :system)
33
34
(local (include-book "misc/assert" :dir :system))
34
35
(local (include-book "../util/arithmetic"))
35
36
(local (include-book "../util/position"))
398
399
                                  ACL2::LIST-FIX-WHEN-TRUE-LISTP
399
400
                                  double-containment
400
401
                                  MEMBER-EQUAL-WHEN-MEMBER-EQUAL-OF-CDR-UNDER-IFF
401
 
                                  MEMBER-EQUAL-WHEN-ALL-EQUALP
 
402
                                  acl2::MEMBER-EQUAL-WHEN-ALL-EQUALP
402
403
                                  acl2::subsetp-trans
403
404
                                  acl2::subsetp-trans2
404
405
 
829
830
     (assert! (not (vl-emodwire-p 'vl::foo))))))
830
831
 
831
832
 
832
 
 
833
 
(deflist vl-emodwirelist-p (x)
834
 
  (vl-emodwire-p x)
 
833
(define vl-emodwire-fix ((x vl-emodwire-p))
 
834
  :returns (x-prime vl-emodwire-p)
 
835
  :inline t
 
836
  :hooks nil
 
837
  (mbe :logic (if (vl-emodwire-p x) x 'acl2::bad-default-emodwire)
 
838
       :exec x)
 
839
  ///
 
840
  (defthm vl-emodwire-fix-when-vl-emodwire-p
 
841
    (implies (vl-emodwire-p x)
 
842
             (equal (vl-emodwire-fix x) x)))
 
843
 
 
844
  (fty::deffixtype vl-emodwire :pred vl-emodwire-p :fix vl-emodwire-fix
 
845
    :equiv vl-emodwire-equiv :define t))
 
846
 
 
847
 
 
848
(fty::deflist vl-emodwirelist :elt-type vl-emodwire
835
849
  :elementp-of-nil nil
836
850
  :parents (exploding-vectors)
837
 
  :rest
838
 
  ((defthm symbol-listp-when-vl-emodwirelist-p
839
 
     (implies (vl-emodwirelist-p x)
840
 
              (equal (symbol-listp x)
841
 
                     (true-listp x))))
842
 
 
843
 
   (defthm member-of-nil-when-vl-emodwirelist-p
844
 
     (implies (vl-emodwirelist-p x)
845
 
              (not (member-equal nil x))))))
846
 
 
847
 
 
848
 
(deflist vl-emodwirelistlist-p (x)
849
 
  (vl-emodwirelist-p x)
850
 
  :guard t
 
851
  ///
 
852
  (local (in-theory (enable vl-emodwirelist-p)))
 
853
  (defthm symbol-listp-when-vl-emodwirelist-p
 
854
    (implies (vl-emodwirelist-p x)
 
855
             (equal (symbol-listp x)
 
856
                    (true-listp x))))
 
857
 
 
858
  (defthm member-of-nil-when-vl-emodwirelist-p
 
859
    (implies (vl-emodwirelist-p x)
 
860
             (not (member-equal nil x)))))
 
861
 
 
862
 
 
863
(fty::deflist vl-emodwirelistlist :elt-type vl-emodwirelist
851
864
  :elementp-of-nil t
852
865
  :parents (exploding-vectors)
853
866
  :short "A list of @(see vl-emodwire-p) lists."
855
868
  :long "<p>These are notably used as the @(':i') and @(':o') patterns for
856
869
modules; see @(see modinsts-to-eoccs) for details.</p>"
857
870
 
858
 
  :rest
859
 
  ((defthm vl-emodwirelist-p-of-flatten
860
 
     (implies (vl-emodwirelistlist-p x)
861
 
              (vl-emodwirelist-p (flatten x))))))
 
871
  ///
 
872
  (local (in-theory (enable vl-emodwirelistlist-p)))
 
873
  (defthm vl-emodwirelist-p-of-flatten
 
874
    (implies (vl-emodwirelistlist-p x)
 
875
             (vl-emodwirelist-p (flatten x)))))
862
876
 
863
877
 
864
878
(defsection vl-emodwire