1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
|
(in-package "BCV")
(include-book "../BCV/typechecker")
(acl2::set-verify-guards-eagerness 0)
;; Wed Jul 13 14:25:51 2005
(defun make-static-class-decl (cn super cp fs ms is as)
(LIST 'CLASS cn super
(CONS 'CONSTANT_POOL CP)
(CONS 'FIELDS fs)
(CONS 'METHODS ms)
(CONS 'INTERFACES is)
(CONS 'ACCESSFLAGS as)))
;; (defun make-static-class-decl (cn super cp fs ms is as ats)
;; (LIST 'CLASS cn super
;; (CONS 'CONSTANT_POOL CP)
;; (CONS 'FIELDS fs)
;; (CONS 'METHODS ms)
;; (CONS 'INTERFACES is)
;; (CONS 'ACCESSFLAGS as)
;; (CONS 'ATTRIBUTES ats)))
(defun wff-scl-decl-guard-weak (scl-decl)
(and (true-listp scl-decl)
(equal (len scl-decl) 8)
(consp (nth 4 scl-decl))
(consp (nth 5 scl-decl))
(consp (nth 6 scl-decl))
(consp (nth 7 scl-decl))))
;; (defun wff-scl-decl-guard-weak (scl-decl)
;; (and (true-listp scl-decl)
;; (equal (len scl-decl) 9)
;; (consp (nth 4 scl-decl))
;; (consp (nth 5 scl-decl))
;; (consp (nth 6 scl-decl))
;; (consp (nth 7 scl-decl))
;; (consp (nth 8 scl-decl))))
(defun scl-decl-bcv2jvm (scl-decl)
(declare (xargs :guard (wff-scl-decl-guard-weak scl-decl)))
(make-static-class-decl
(classClassName scl-decl)
(classSuperClassName scl-decl)
(classConstantPool scl-decl)
(classFields scl-decl)
(classMethods scl-decl)
(classInterfaces scl-decl)
(classAccessFlags scl-decl)))
;; (defun scl-decl-bcv2jvm (scl-decl)
;; (declare (xargs :guard (wff-scl-decl-guard-weak scl-decl)))
;; (make-static-class-decl
;; (classClassName scl-decl)
;; (classSuperClassName scl-decl)
;; (classConstantPool scl-decl)
;; (classFields scl-decl)
;; (classMethods scl-decl)
;; (classInterfaces scl-decl)
;; (classAccessFlags scl-decl)
;; (classAttributes scl-decl)))
(defun scl-bcv2jvm (scl)
(if (endp scl) nil
(cons (scl-decl-bcv2jvm (car scl))
(scl-bcv2jvm (cdr scl)))))
(defun scl-jvm2bcv (raw-scl)
(if (endp raw-scl) nil
(cons (make-class-def (car raw-scl))
(scl-jvm2bcv (cdr raw-scl)))))
(defun good-scl (scl)
(and (not (isClassTerm
(class-by-name
(classSuperClassName
(class-by-name "java.lang.Object" scl))
scl)))
(not (isClassTerm (class-by-name nil scl)))
(equal (scl-jvm2bcv (scl-bcv2jvm scl)) scl)))
;;Fri Jul 15 18:17:33 2005
|