[acl2-books] r989 committed - ...
acl2-...@googlecode.com
Author: sswords
Date: Tue Feb 28 11:49:40 2012
Log:
- Updated hash-stobjs book to work in current acl2.
- Added tools/easy-simplify.lisp, providing a simple interface for term
rewriting.
- Adjusted aig-cases macro for better performance
- Adjusted simple-one-way-unify so that it provides information about why
it failed
- Fixed bug in xf-stmt-rewrite that prevented some logically-empty case
statements
from disappearing.
http://code.google.com/p/acl2-books/source/detail?r=989
Added:
/trunk/centaur/misc/make-list.lisp
/trunk/tools/easy-simplify.lisp
Modified:
/trunk/add-ons/hash-stobjs.lisp
/trunk/centaur/aig/base.lisp
/trunk/centaur/vl/transforms/xf-stmt-rewrite.lisp
/trunk/clause-processors/unify-subst.lisp
=======================================
--- /dev/null
+++ /trunk/centaur/misc/make-list.lisp Tue Feb 28 11:49:40 2012
@@ -0,0 +1,16 @@
+
+(in-package "ACL2")
+
+;; This simply provides a non-tail-recursive way of reasoning about
+;; make-list-ac, which is the macroexpansion of make-list.
+
+(defthm make-list-ac-redef
+ (equal (make-list-ac n val ac)
+ (if (zp n)
+ ac
+ (cons val (make-list-ac (1- n) val ac))))
+ :rule-classes ((:definition
+ :clique (make-list-ac)
+ :controller-alist ((make-list-ac t nil nil)))))
+
+(in-theory (disable make-list-ac))
=======================================
--- /dev/null
+++ /trunk/tools/easy-simplify.lisp Tue Feb 28 11:49:40 2012
@@ -0,0 +1,113 @@
+
+
+(in-package "ACL2")
+
+(include-book "bstar")
+
+;; This provides a straightforward interface for simplifying a term. It
uses
+;; the proof checker's pc-rewrite* function. It can handle rewriting under
+;; some hypotheses, under a user-provided equivalence relation,
+
+
+(defun if-nest-to-hyp-list (x)
+ (cond ((equal x ''t) nil)
+ ((or (atom x)
+ (not (eq (car x) 'if))
+ (not (equal (fourth x) ''nil)))
+ (list x))
+ (t (append (if-nest-to-hyp-list (second x))
+ (if-nest-to-hyp-list (third x))))))
+
+
+;; takes a translated term and an implicitly conjoined list of translated
hyps
+(defun easy-simplify-term1-fn (term hyps hints equiv
+ normalize rewrite
+ repeat
+ backchain-limit
+ state)
+ (declare (XargS :mode :program :stobjs state))
+ (b* ((world (w state))
+
+ ((er hint-settings)
+ (translate-hint-settings
+ 'simp-term "Goal" hints 'easy-simplify-term world state))
+ (ens (ens state))
+ (base-rcnst
+ (change rewrite-constant
+ *empty-rewrite-constant*
+ :current-enabled-structure ens
+ :force-info t))
+ ((er rcnst)
+ (load-hint-settings-into-rcnst
+ hint-settings base-rcnst nil world 'easy-simplify-term state))
+ (ens (access rewrite-constant rcnst :current-enabled-structure))
+ ((mv flg hyps-type-alist ?ttree)
+ (hyps-type-alist hyps ens world state))
+ ((when flg)
+ (mv "Contradiction in the hypotheses"
+ nil state))
+ ((mv ?step-limit new-term ?new-ttree state)
+ (pc-rewrite*
+ term hyps-type-alist
+ (if (eq equiv 'equal)
+ nil
+ (list (make congruence-rule
+ :rune *fake-rune-for-anonymous-enabled-rule*
+ :nume nil
+ :equiv equiv)))
+ (eq equiv 'iff)
+ world rcnst nil nil normalize rewrite ens state
+ repeat backchain-limit
+ (initial-step-limit world state))))
+ (value new-term)))
+
+(defun easy-simplify-term-fn (term hyp-term hints equiv
+ normalize rewrite repeat backchain-limit
state)
+ (declare (XargS :mode :program :stobjs state))
+ (b* ((world (w state))
+ ((er trans-term)
+ (translate term t nil t 'easy-simplify-term world state))
+ ((er trans-hyp-term)
+ (translate hyp-term t nil t 'easy-simplify-term world state))
+ ;; bozo find out how ACL2 does this, if it does
+ (hyps (if-nest-to-hyp-list trans-hyp-term))
+ ((er new-term)
+ (easy-simplify-term1-fn
+ trans-term hyps hints equiv normalize rewrite repeat
backchain-limit
+ state)))
+ (value (untranslate new-term nil (w state)))))
+
+(defmacro easy-simplify-term (term &key
+ (hyp 't)
+ hint
+ (equiv 'equal)
+ (normalize 't)
+ (rewrite 't)
+ (repeat '1000)
+ (backchain-limit '1000))
+ ":doc-section programming
+ Easy-simplify-term: simple interface for simplifying a term.~/
+
+Usage:
+~bv[]
+ (easy-simplify-term (my-fn (foo) (bar baz))
+ ;; optional keyword args:
+ :hyp (and (integerp baz) (<= 0 baz))
+ :hint (:in-theory (enable my-fn) :expand ((foo)))
+ :equiv equal
+ :normalize t
+ :rewrite t
+ :repeat 555
+ :backchain-limit 5)
+~ev[]
+
+ Important NOTE: The HINT keyword should be given a hint keyword/val list,
+ as in the example above, NOT a list of subgoal or computed hints,
+ e.g. ((\"Goal\" :foo)). ~/
+
+ Simplifies a term under the given hypothesis and equivalence context,
+ with guidance from the given hint."
+ `(easy-simplify-term-fn
+ ',term ',hyp ',hint ',equiv
+ ',normalize ',rewrite ',repeat ',backchain-limit
+ state))
=======================================
--- /trunk/add-ons/hash-stobjs.lisp Thu Oct 16 13:51:07 2008
+++ /trunk/add-ons/hash-stobjs.lisp Tue Feb 28 11:49:40 2012
@@ -40,14 +40,6 @@
;; have nothing to do with the performance in raw Lisp, and arguably
;; we care more about ease of proving guard conjectures than we do
;; about how well they perform in the logic.
-(defun easy-assoc (x al)
- (declare (xargs :guard t))
- (if (atom al)
- nil
- (if (and (consp (car al))
- (equal x (caar al)))
- (car al)
- (easy-assoc x (cdr al)))))
(defun remove-assoc (x al)
(declare (xargs :guard t))
@@ -71,12 +63,12 @@
(count-keys (cdr al)))))
(defthm not-assoc-remove-assoc
- (not (easy-assoc k (remove-assoc k al))))
+ (not (hons-assoc-equal k (remove-assoc k al))))
(defthm assoc-remove-assoc-diff
(implies (not (equal j k))
- (equal (easy-assoc k (remove-assoc j al))
- (easy-assoc k al))))
+ (equal (hons-assoc-equal k (remove-assoc j al))
+ (hons-assoc-equal k al))))
(defthm remove-assoc-repeat
(equal (remove-assoc k (remove-assoc k al))
@@ -90,45 +82,28 @@
(defthm count-keys-remove-assoc
(equal (count-keys (remove-assoc k al))
- (if (consp (easy-assoc k al))
+ (if (consp (hons-assoc-equal k al))
(1- (count-keys al))
(count-keys al))))
(defthm count-keys-cons
(equal (count-keys (cons (cons k v) al))
- (if (consp (easy-assoc k al))
+ (if (consp (hons-assoc-equal k al))
(count-keys al)
(+ 1 (count-keys al)))))
-(defconst *report-bad-hons-equal-hash-discipline* nil)
-
-;; only works under the hood
-(defmacro hons-copy-for-ht-key (x)
- `(let ((hons-copy-for-ht-key-key ,x))
- (if (atom hons-copy-for-ht-key-key)
- (maybe-str-hash hons-copy-for-ht-key-key)
- (if (honsp hons-copy-for-ht-key-key)
- hons-copy-for-ht-key-key
- (if *report-bad-hons-equal-hash-discipline*
- (progn (cw "Non-HONS key for hons-equal hash table~%")
- (break$)
- (hons-copy hons-copy-for-ht-key-key))
- (hons-copy hons-copy-for-ht-key-key))))))
-
#||
;; Using this example stobj definition, we'll illustrate the logical
;; definitions of the functions used to access and update the table.
(defstobj htable
- (tab :type (hash-table eql
- ;; equal or hons-equal also possible.
- )))
+ (tab :type (hash-table eql))) ;; or (hash-table equal)
(defun tabp
(declare (xargs :guard t))
- ;; Because we made the guards on easy-assoc and remove-assoc T, we
+ ;; Because we made the guards on hons-assoc-equal and remove-assoc T, we
;; don't need to constrain what tabp is logically.
t)
@@ -146,14 +121,14 @@
(declare (xargs :guard (and (htablep htable)
;; eqlablep only in EQL version
(eqlablep k))))
- (cdr (easy-assoc k (nth 0 htable))))
+ (cdr (hons-assoc-equal k (nth 0 htable))))
;; BOUNDP, logic:
(defun tab-boundp (k htable)
(declare (xargs :guard (and (htablep htable)
;; eqlablep only in EQL version
(eqlablep k))))
- (consp (easy-assoc k (nth 0 htable))))
+ (consp (hons-assoc-equal k (nth 0 htable))))
;; GET?, logic:
(defun tab-get? (k htable)
@@ -184,8 +159,23 @@
;; CLEAR, logic:
(defun tab-clear (htable)
+ (declare (xargs :guard (htablep htable)))
(update-nth 0 nil htable))
+(defun tab-init (size rehash-size rehash-threshold htable)
+ (declare (xargs :guard (and (htablep htable)
+ (or (natp size)
+ (not size))
+ (or (and (rationalp rehash-size)
+ (< 1 rehash-size))
+ (not rehash-size))
+ (or (and (rationalp rehash-threshold)
+ (<= 0 rehash-threshold)
+ (<= rehash-threshold 1))
+ (not rehash-threshold)))))
+ (declare (ignore size rehash-size rehash-threshold))
+ (update-nth 0 nil htable))
+
;; Theorems about the interactions of the functions above: Our
;; approach is sound if these theorems completely and accurately model
;; the functionality of a Common Lisp hash table, modulo assumptions
@@ -203,6 +193,11 @@
;; access of htable,
;; Induction case 2: (tab-rem j htable), j not equal k, reduces to
;; access of htable.
+
+(defthm tab-init-is-tab-clear
+ (equal (tab-init size rehash-size rehash-threshold htable)
+ (tab-clear htable)))
+
(defthm tab-get-tab-boundp
(implies (tab-get k htable)
(tab-boundp k htable)))
@@ -302,6 +297,18 @@
(clrhash (svref htable 0))
htable)
+(defun tab-init (size rehash-size rehash-threshold htable)
+ (setf (svref htable 0)
+ (make-hash-table
+ :size (or size 60)
+ :rehash-size (if rehash-size
+ (float rehash-size)
+ (float 17/10))
+ :rehash-threshold (if rehash-threshold
+ (float rehash-threshold)
+ (float 3/4))))
+ htable)
+
||#
@@ -309,12 +316,10 @@
(defttag hash-stobjs)
-(include-book "hacking/hacker" :dir :system)
-
(program)
(set-state-ok t)
-(with-redef-allowed
+(redef+)
(defun defstobj-fnname (root key1 key2 renaming-alist)
; This has been moved from other-events.lisp, where other stobj-related
@@ -383,6 +388,9 @@
(:count
(and (eq key2 :hash-table)
(packn-pos (list root "-COUNT") root)))
+ (:init
+ (and (eq key2 :hash-table)
+ (packn-pos (list root "-INIT") root)))
(:clear
(and (eq key2 :hash-table)
(packn-pos (list root "-CLEAR") root)))
@@ -397,7 +405,11 @@
-(defun defstobj-fields-template (field-descriptors renaming)
+(defun defstobj-fields-template (field-descriptors renaming wrld)
+
+; Note: Wrld may be a world, nil, or (in raw Lisp only) the
symbol :raw-lisp.
+; See fix-stobj-array-type.
+
(cond
((endp field-descriptors) nil)
(t
@@ -435,11 +447,15 @@
(remove-name (defstobj-fnname field :remove key2 renaming))
(count-name (defstobj-fnname field :count key2 renaming))
(clear-name (defstobj-fnname field :clear key2 renaming))
+ (init-name (defstobj-fnname field :init key2 renaming))
; >---
(resize-name (defstobj-fnname field :resize key2 renaming))
(length-name (defstobj-fnname field :length key2 renaming)))
(cons (list fieldp-name
- type
+ (cond ((and (consp type)
+ (eq (car type) 'array))
+ (fix-stobj-array-type type wrld))
+ (t type))
init
accessor-name
updater-name
@@ -452,9 +468,11 @@
remove-name
count-name
clear-name
+ init-name
; >---
)
- (defstobj-fields-template (cdr field-descriptors)
renaming))))))
+ (defstobj-fields-template
+ (cdr field-descriptors) renaming wrld))))))
(defun defstobj-raw-init-fields (ftemps)
@@ -487,13 +505,13 @@
(cons `(make-hash-table
:test
,(case hash-test
- ((eql hons-equal) ''eql)
+ (eql ''eql)
(equal
;; Is this safe?
''equal)
(t (er hard hash-test
"The hash test should be either ~
-EQL, EQUAL, or HONS-EQUAL.~%")))
+EQL or EQUAL.~%")))
:size ,hash-init-size)
(defstobj-raw-init-fields (cdr ftemps))))
; >---
@@ -640,6 +658,7 @@
(remove-name (nth 10 field-template))
(count-name (nth 11 field-template))
(clear-name (nth 12 field-template))
+ (init-name (nth 13 field-template))
; >---
)
(cond
@@ -703,7 +722,7 @@
(eqlablep k))
`(,top-recog ,var))
:verify-guards t))
- (cdr (easy-assoc k (nth ,n ,var))))
+ (cdr (hons-assoc-equal k (nth ,n ,var))))
(,updater-name
(k v ,var)
(declare (xargs :guard ,(if (eq hash-test 'eql)
@@ -719,7 +738,7 @@
(eqlablep k))
`(,top-recog ,var))
:verify-guards t))
- (consp (easy-assoc k (nth ,n ,var))))
+ (consp (hons-assoc-equal k (nth ,n ,var))))
(,accessor?-name
(k ,var)
@@ -745,6 +764,20 @@
(,clear-name
(,var)
(declare (xargs :guard (,top-recog ,var)))
+ (update-nth ,n nil ,var))
+ (,init-name
+ (size rehash-size rehash-threshold ,var)
+ (declare (xargs :guard (and (,top-recog ,var)
+ (or (natp size)
+ (not size))
+ (or (and (rationalp rehash-size)
+ (< 1 rehash-size))
+ (not rehash-size))
+ (or (and (rationalp
rehash-threshold)
+ (<= 0 rehash-threshold)
+ (<= rehash-threshold 1))
+ (not rehash-threshold))))
+ (ignorable size rehash-size rehash-threshold))
(update-nth ,n nil ,var)))
(defstobj-field-fns-axiomatic-defs
top-recog var (+ n 1) (cdr ftemps) wrld)))
@@ -818,7 +851,6 @@
(if (array-etype-is-fixnum-type array-etype)
'fix-aref
vref)))
- (max-index (and arrayp (1- *expt2-28*)))
(accessor-name (nth 3 field-template))
(updater-name (nth 4 field-template))
(length-name (nth 5 field-template))
@@ -832,6 +864,7 @@
(remove-name (nth 10 field-template))
(count-name (nth 11 field-template))
(clear-name (nth 12 field-template))
+ (init-name (nth 13 field-template))
; >---
)
(cond
@@ -841,17 +874,16 @@
(k ,var)
,@(and inline (list *stobj-inline-declare*))
(values (gethash ,(if (eq hash-test 'hons-equal)
- `(hons-copy-for-ht-key k)
+ `(hons-copy k)
'k)
(the 'hash-table (svref ,var ,n)))))
(,updater-name
(k v ,var)
,@(and inline (list *stobj-inline-declare*))
(progn
- #+(and hons (not acl2-loop-only))
- (memoize-flush ,var)
+ #+hons (memoize-flush ,var)
(setf (gethash ,(if (eq hash-test 'hons-equal)
- `(hons-copy-for-ht-key k)
+ `(hons-copy k)
'k)
(the 'hash-table (svref ,var ,n)))
v)
@@ -861,18 +893,21 @@
,@(and inline (list *stobj-inline-declare*))
(multiple-value-bind (val boundp)
(gethash ,(if (eq hash-test 'hons-equal)
- `(hons-copy-for-ht-key k)
+ `(hons-copy k)
'k)
(the 'hash-table (svref ,var ,n)))
(declare (ignore val))
- boundp))
+ (if boundp t nil)))
(,accessor?-name
(k ,var)
,@(and inline (list *stobj-inline-declare*))
- (gethash ,(if (eq hash-test 'hons-equal)
- `(hons-copy-for-ht-key k)
- 'k)
- (the 'hash-table (svref ,var ,n))))
+ (multiple-value-bind
+ (val boundp)
+ (gethash ,(if (eq hash-test 'hons-equal)
+ `(hons-copy k)
+ 'k)
+ (the 'hash-table (svref ,var ,n)))
+ (mv val (if boundp t nil))))
(,remove-name
(k ,var)
,@(and inline (list *stobj-inline-declare*))
@@ -880,7 +915,7 @@
#+(and hons (not acl2-loop-only))
(memoize-flush ,var)
(remhash ,(if (eq hash-test 'hons-equal)
- `(hons-copy-for-ht-key k)
+ `(hons-copy k)
'k)
(the 'hash-table (svref ,var ,n)))
,var))
@@ -895,6 +930,28 @@
#+(and hons (not acl2-loop-only))
(memoize-flush ,var)
(clrhash (svref ,var ,n))
+ ,var))
+ (,init-name
+ (size rehash-size rehash-threshold ,var)
+ ,@(and inline (list *stobj-inline-declare*))
+ (progn
+ #+(and hons (not acl2-loop-only))
+ (memoize-flush ,var)
+ (setf (svref ,var ,n)
+ (make-hash-table
+ :test ',(case hash-test
+ (eql 'eql)
+ (equal 'equal)
+ (t (er hard hash-test
+ "The hash test should be either ~
+EQL or EQUAL.~%")))
+ :size (or size 60)
+ :rehash-size (if rehash-size
+ (float rehash-size)
+ (float 17/10))
+ :rehash-threshold (if rehash-threshold
+ (float rehash-threshold)
+ (float 3/4))))
,var))))
; >---
(arrayp
@@ -904,7 +961,7 @@
,@(if (not resizable)
`((declare (ignore ,var))
,array-length)
- `((the (integer 0 ,max-index)
+ `((the (and fixnum (integer 0 *))
(length (svref ,var ,n))))))
(,resize-name
(k ,var)
@@ -920,14 +977,16 @@
,var))
`((if (not (and (integerp k)
(>= k 0)
- (< k ,max-index)))
+ (< k array-dimension-limit)))
(hard-error
',resize-name
"Attempted array resize failed because the
requested ~
- size ~x0 was not an integer between 0 and (1-
(expt ~
- 2 28)). These bounds on array sizes are fixed by ~
- ACL2."
- (list (cons #\0 k)))
+ size ~x0 was not a nonnegative integer less than
the ~
+ value of Common Lisp constant
array-dimension-limit, ~
+ which is ~x1. These bounds on array sizes are
fixed ~
+ by ACL2."
+ (list (cons #\0 k)
+ (cons #\1 array-dimension-limit)))
(let* ((old (svref ,var ,n))
(min-index (if (< k (length old))
k
@@ -949,29 +1008,27 @@
',init
:element-type
',array-etype)))
- #+(and hons (not acl2-loop-only))
- (memoize-flush ,var)
+ #+hons (memoize-flush ,var)
(setf (svref ,var ,n)
(,(pack2 'stobj-copy-array- fix-vref)
old new 0 min-index))
,var)))))
(,accessor-name
(i ,var)
- (declare (type (integer 0 ,max-index) i))
+ (declare (type (and fixnum (integer 0 *)) i))
,@(and inline (list *stobj-inline-declare*))
(the ,array-etype
(,vref (the ,simple-type (svref ,var ,n))
- (the (integer 0 ,max-index) i))))
+ (the (and fixnum (integer 0 *)) i))))
(,updater-name
(i v ,var)
- (declare (type (integer 0 ,max-index) i)
+ (declare (type (and fixnum (integer 0 *)) i)
(type ,array-etype v))
,@(and inline (list *stobj-inline-declare*))
(progn
- #+(and hons (not acl2-loop-only))
- (memoize-flush ,var)
+ #+hons (memoize-flush ,var)
(setf (,vref (the ,simple-type (svref ,var ,n))
- (the (integer 0 ,max-index) i))
+ (the (and fixnum (integer 0 *)) i))
(the ,array-etype v))
,var))))
((equal type t)
@@ -981,9 +1038,9 @@
(,updater-name (v ,var)
,@(and inline (list *stobj-inline-declare*))
(progn
- #+(and hons (not acl2-loop-only))
- (memoize-flush ,var)
- (setf (svref ,var ,n) v) ,var))))
+ #+hons (memoize-flush ,var)
+ (setf (svref ,var ,n) v)
+ ,var))))
(t
`((,accessor-name (,var)
,@(and inline (list *stobj-inline-declare*))
@@ -995,8 +1052,7 @@
(declare (type ,type v))
,@(and inline (list *stobj-inline-declare*))
(progn
- #+(and hons (not acl2-loop-only))
- (memoize-flush ,var)
+ #+hons (memoize-flush ,var)
(setf (aref (the (simple-array ,type (1))
(svref ,var ,n))
0)
@@ -1058,30 +1114,30 @@
(true-listp (caddr type))
(equal (length (caddr type)) 1)))
(er soft ctx
- "When a field descriptor specifies an ARRAY :type, ~
- the type must be of the form (ARRAY etype (n)). ~
- Note that we only support single-dimensional arrays. ~
- The purported ARRAY :type ~x0 for the ~x1 field of ~
- ~x2 is not of this form."
+ "When a field descriptor specifies an ARRAY :type, the
type ~
+ must be of the form (ARRAY etype (n)). Note that we only
~
+ support single-dimensional arrays. The purported ARRAY ~
+ :type ~x0 for the ~x1 field of ~x2 is not of this form."
type field name))
- (t (let* ((etype (cadr type))
+ (t (let* ((type0 (fix-stobj-array-type type wrld))
+ (etype (cadr type0))
(etype-term (translate-declaration-to-guard
etype 'x wrld))
- (n (car (caddr type))))
+ (n (car (caddr type0))))
(cond
((null etype-term)
(er soft ctx
"The element type specified for the ~x0 field of ~
- ~x1, namely ~x0, is not recognized by ACL2 as a ~
+ ~x1, namely ~x2, is not recognized by ACL2 as a ~
type-spec. See :DOC type-spec."
field name type))
- ((not (and (integerp n)
- (<= 0 n)))
+ ((not (natp n))
(er soft ctx
- "Array dimensions must be non-negative integers. ~
- The :type ~x0 for the ~x1 field of ~x2 is thus ~
+ "An array dimension must be a non-negative integer or
a ~
+ defined constant whose value is a non-negative
integer. ~
+ ~ The :type ~x0 for the ~x1 field of ~x2 is thus ~
illegal."
- type field name))
+ type0 field name))
(t
(er-let*
((pair (simple-translate-and-eval etype-term
@@ -1092,7 +1148,8 @@
etype-term)
ctx
wrld
- state)))
+ state
+ nil)))
; pair is (tterm . val), where tterm is a term and val is its value
; under x<-init.
@@ -1132,7 +1189,7 @@
extension) HONS-EQUAL. The test given was ~
~x0.~%" (and (consp (cdr type))
(cadr type))))
- (t (value nil))))
+ (t (value nil))))
(t (let ((type-term (translate-declaration-to-guard
type 'x wrld)))
(cond
@@ -1152,7 +1209,8 @@
type-term)
ctx
wrld
- state)))
+ state
+ nil)))
; pair is (tterm . val), where tterm is a term and val is its value
; under x<-init.
@@ -1254,6 +1312,7 @@
renaming))
(count-name (defstobj-fnname field :count key2 renaming))
(clear-name (defstobj-fnname field :clear key2 renaming))
+ (init-name (defstobj-fnname field :init key2 renaming))
; >---
(fieldp-name (defstobj-fnname field :recognizer key2 renaming))
(accessor-name (defstobj-fnname field :accessor key2 renaming))
@@ -1292,6 +1351,7 @@
remove-name
count-name
clear-name
+ init-name
names)
names)))
(cons accessor-const-name
@@ -1315,6 +1375,7 @@
(remove-fn (nth 10 (car ftemps)))
(count-fn (nth 11 (car ftemps)))
(clear-fn (nth 12 (car ftemps)))
+ (init-fn (nth 13 (car ftemps)))
;; >---
)
(put-stobjs-in-and-outs1
@@ -1338,32 +1399,38 @@
((and (consp type)
(eq (car type) 'hash-table))
(putprop
- clear-fn 'stobjs-in (list name)
+ init-fn 'stobjs-in (list nil nil nil name)
(putprop
- clear-fn 'stobjs-out (list name)
+ init-fn 'stobjs-out (list name)
(putprop
- count-fn 'stobjs-in (list name)
+ clear-fn 'stobjs-in (list name)
(putprop
- remove-fn 'stobjs-in (list nil name)
+ clear-fn 'stobjs-out (list name)
(putprop
- remove-fn 'stobjs-out (list name)
+ count-fn 'stobjs-in (list name)
(putprop
- accessor?-fn 'stobjs-in (list nil name)
+ remove-fn 'stobjs-in (list nil name)
(putprop
- boundp-fn 'stobjs-in (list nil name)
+ remove-fn 'stobjs-out (list name)
(putprop
- acc-fn 'stobjs-in (list nil name)
+ accessor?-fn 'stobjs-in (list nil name)
(putprop
- upd-fn 'stobjs-in (list nil nil name)
+ boundp-fn 'stobjs-in (list nil name)
(putprop
- upd-fn 'stobjs-out (list name) wrld)))))))))))
+ acc-fn 'stobjs-in (list nil name)
+ (putprop
+ upd-fn 'stobjs-in (list nil nil name)
+ (putprop
+ upd-fn 'stobjs-out (list name) wrld)))))))))))))
(t
(putprop
acc-fn 'stobjs-in (list name)
(putprop
upd-fn 'stobjs-in (list nil name)
(putprop
- upd-fn 'stobjs-out (list name) wrld)))))))))))
+ upd-fn 'stobjs-out (list name) wrld))))))))))
+
+(redef-)
;; Macro for proving theorems like the ones above about a hash field:
@@ -1375,8 +1442,13 @@
(rem (defstobj-fnname field :remove :hash-table renaming))
(count (defstobj-fnname field :count :hash-table renaming))
(clear (defstobj-fnname field :clear :hash-table renaming))
+ (init (defstobj-fnname field :init :hash-table renaming))
(make (defstobj-fnname stobj :creator :hash-table renaming)))
`(progn
+ (defthm ,(packn-pos (list field "-INIT-IS-CLEAR") field)
+ (equal (,init size rehash-size rehash-threshold ,stobj)
+ (,clear ,stobj)))
+
(defthm ,(packn-pos (list field "-GET-BOUNDP") field)
(implies (,get k ,stobj)
(,boundp k ,stobj)))
@@ -1436,3 +1508,108 @@
(equal (,count (,clear ,stobj))
0)))))
+
+
+(local
+ (progn
+
+ (defstobj bigstobj
+ (bigarray :type (array (unsigned-byte 16) (100))
+ :initially 0)
+ (bighash :type (hash-table eql))
+ (slowhash :type (hash-table equal))
+ )
+
+ (make-event
+ (let* ((bigstobj (bighash-put 0 0 bigstobj))
+ (bigstobj (slowhash-put (list 0) 0 bigstobj)))
+ (mv nil '(value-triple :invisible) state bigstobj)))
+
+ (include-book "misc/assert" :dir :system)
+
+ (assert! (equal (bighash-get 0 bigstobj) 0))
+ (assert! (equal (slowhash-get '(0) bigstobj) 0))
+
+ (defun init-stuff (n bigstobj state)
+ (declare (xargs :stobjs (bigstobj state)
+ :verify-guards nil
+ :guard (natp n)))
+ (if (zp n)
+ (mv bigstobj state)
+ (mv-let (rnd state) (random$ 10000 state)
+ (let* ((bigstobj (update-bigarrayi n rnd bigstobj))
+ (bigstobj (bighash-put n rnd bigstobj))
+ (bigstobj (slowhash-put (list n) rnd bigstobj)))
+ (init-stuff (- n 1) bigstobj state)))))
+
+ (make-event
+ (mv-let (bigstobj state)
+ (init-stuff 99 bigstobj state)
+ (mv nil '(value-triple :invisible) state bigstobj)))
+
+ (assert! (equal (bighash-count bigstobj) 100))
+ (assert! (equal (slowhash-count bigstobj) 100))
+
+ (make-event
+ (let* ((bigstobj (slowhash-put (cons 1 2) 3 bigstobj))
+ (bigstobj (slowhash-put (cons 1 2) 4 bigstobj)))
+ (mv nil '(value-triple :invisible) state bigstobj)))
+
+ (assert! (equal (slowhash-get (cons 1 2) bigstobj) 4))
+ (assert! (equal (slowhash-count bigstobj) 101))
+
+
+
+ (defun check-same (n bigstobj)
+ (declare (xargs :stobjs (bigstobj)
+ :verify-guards nil
+ :guard (natp n)))
+ (if (zp n)
+ t
+ (let ((expect (bigarrayi n bigstobj)))
+ (and (equal (bighash-get n bigstobj) expect)
+ (equal (slowhash-get (list n) bigstobj) expect)
+ (equal (bighash-boundp n bigstobj) t)
+ (equal (slowhash-boundp (list n) bigstobj) t)
+ (equal (mv-list 2 (bighash-get? n bigstobj)) (list expect t))
+ (equal (mv-list 2 (slowhash-get? (list n) bigstobj)) (list
expect
+
t))
+ (check-same (- n 1) bigstobj)))))
+
+ (assert! (check-same 99 bigstobj))
+
+ (assert! (not (bighash-boundp 101 bigstobj)))
+ (assert! (equal (mv-list 2 (bighash-get? 101 bigstobj)) (list nil nil)))
+
+ (assert! (not (slowhash-boundp 101 bigstobj)))
+ (assert! (equal (mv-list 2 (slowhash-get? 101 bigstobj)) (list nil
nil)))
+
+ (assert! (not (slowhash-boundp (list 101) bigstobj)))
+ (assert! (equal (mv-list 2 (slowhash-get? (list 101) bigstobj)) (list
nil nil)))
+
+ (make-event
+ (let* ((bigstobj (bighash-rem 3 bigstobj))
+ (bigstobj (slowhash-rem (list 3) bigstobj)))
+ (mv nil '(value-triple :invisible) state bigstobj)))
+
+ (assert! (not (bighash-boundp 3 bigstobj)))
+ (assert! (not (slowhash-boundp (list 3) bigstobj)))
+
+ (assert! (equal (slowhash-count bigstobj) 100))
+ (assert! (equal (bighash-count bigstobj) 99))
+
+ (make-event
+ (let* ((bigstobj (slowhash-clear bigstobj))
+ (bigstobj (bighash-init 10000 nil nil bigstobj)))
+ (mv nil '(value-triple :invisible) state bigstobj)))
+
+ (assert! (equal (bighash-count bigstobj) 0))
+ (assert! (equal (slowhash-count bigstobj) 0))
+ (assert! (equal (bighash-get 5 bigstobj) nil))
+ (assert! (equal (slowhash-get (list 5) bigstobj) nil))
+
+ ))
+
+
+
+
=======================================
--- /trunk/centaur/aig/base.lisp Fri Dec 23 09:58:47 2011
+++ /trunk/centaur/aig/base.lisp Tue Feb 28 11:49:40 2012
@@ -225,9 +225,10 @@
(defmacro aig-cases (x &key true false var inv and)
`(let ((aig-cases-var ,x))
(cond
- ((eq aig-cases-var t) ,true)
- ((eq aig-cases-var nil) ,false)
- ((atom aig-cases-var) ,var)
+ ((atom aig-cases-var)
+ (cond ((eq aig-cases-var t) ,true)
+ ((eq aig-cases-var nil) ,false)
+ (t ,var)))
((eq (cdr aig-cases-var) nil) ,inv)
(t ,and)))))
=======================================
--- /trunk/centaur/vl/transforms/xf-stmt-rewrite.lisp Tue Apr 19 10:19:56
2011
+++ /trunk/centaur/vl/transforms/xf-stmt-rewrite.lisp Tue Feb 28 11:49:40
2012
@@ -294,6 +294,7 @@
(and (vl-fast-nullstmt-p (car x))
(vl-stmtlist-all-null-p (cdr x)))))
+
(defsection vl-casestmt-rewrite
(defund vl-casestmt-rewrite (casetype test exprs bodies default atts)
@@ -319,10 +320,10 @@
(vl-atts-p atts))))
(if (and (vl-fast-nullstmt-p default)
(vl-stmtlist-all-null-p bodies))
-;; All statements are null, just turn into null.
+ ;; All statements are null, just turn into null.
(make-vl-nullstmt)
-;; Otherwise don't change it. Eventually convert all case statements
-;; into if statements?
+ ;; Otherwise don't change it. Eventually convert all case statements
+ ;; into if statements?
(make-vl-casestmt :casetype casetype
:test test
:exprs exprs
@@ -659,6 +660,8 @@
(exprs (vl-casestmt->exprs x))
(bodies (vl-casestmt->bodies x))
(default (vl-casestmt->default x))
+ ((mv warnings bodies) (vl-stmtlist-rewrite bodies
unroll-limit warnings))
+ ((mv warnings default) (vl-stmt-rewrite default
unroll-limit warnings))
(x-prime (vl-casestmt-rewrite casetype
test exprs
bodies
default atts)))
(mv warnings x-prime)))
=======================================
--- /trunk/clause-processors/unify-subst.lisp Fri Sep 3 17:58:14 2010
+++ /trunk/clause-processors/unify-subst.lisp Tue Feb 28 11:49:40 2012
@@ -182,22 +182,23 @@
(cond ((null pat)
(if (eq term nil)
(mv t alist)
- (mv nil alist)))
+ (mv nil (cons (cons pat term) alist))))
((atom pat)
(let ((pair (assoc-equal pat alist)))
(if pair
(if (equal term (cdr pair))
(mv t alist)
- (mv nil alist))
+ (mv nil (cons (cons pat term) alist)))
(mv t (cons (cons pat term) alist)))))
- ((atom term) (mv nil alist))
+ ((atom term)
+ (mv nil (cons (cons pat term) alist)))
((eq (car pat) 'quote)
(if (equal pat term)
(mv t alist)
- (mv nil alist)))
+ (mv nil (cons (cons pat term) alist))))
((equal (car pat) (car term))
(simple-one-way-unify-lst (cdr pat) (cdr term) alist))
- (t (mv nil alist))))
+ (t (mv nil (cons (cons pat term) alist)))))
(defun simple-one-way-unify-lst (pat term alist)
(declare (xargs :guard (and (pseudo-term-listp pat)
(pseudo-term-listp term)
@@ -281,14 +282,18 @@
(defthm-simple-one-way-unify-flag
assoc-one-way-unify-lemma
- (simple-one-way-unify
- (implies (assoc-equal k alist)
+ (defthm assoc-equal-of-simple-one-way-unify-preserved
+ (implies (and (assoc-equal k alist)
+ (mv-nth 0 (simple-one-way-unify pat x alist)))
(equal (assoc-equal k (mv-nth 1 (simple-one-way-unify pat x
alist)))
- (assoc-equal k alist))))
- (simple-one-way-unify-lst
- (implies (assoc-equal k alist)
- (equal (assoc-equal k (mv-nth 1 (simple-one-way-unify-lst pat
x alist)))
- (assoc-equal k alist))))
+ (assoc-equal k alist)))
+ :flag simple-one-way-unify)
+ (defthm assoc-equal-of-simple-one-way-unify-lst-preserved
+ (implies (and (assoc-equal k alist)
+ (mv-nth 0 (simple-one-way-unify-lst pat x alist)))
+ (equal (assoc-equal k (mv-nth 1 (simple-one-way-unify-lst pat
x alist)))
+ (assoc-equal k alist)))
+ :flag simple-one-way-unify-lst)
:hints (("goal" :induct (simple-one-way-unify-flag flag pat x alist))))
@@ -318,13 +323,15 @@
(defthm-simple-term-vars-flag
substitute-into-one-way-unify-reduce-lemma
(simple-term-vars
- (implies (all-keys-bound (simple-term-vars term) alist)
+ (implies (and (all-keys-bound (simple-term-vars term) alist)
+ (mv-nth 0 (simple-one-way-unify pat x alist)))
(equal (substitute-into-term
term (mv-nth 1 (simple-one-way-unify pat x alist)))
(substitute-into-term term alist)))
:name substitute-into-one-way-unify-reduce)
(simple-term-vars-lst
- (implies (all-keys-bound (simple-term-vars-lst term) alist)
+ (implies (and (all-keys-bound (simple-term-vars-lst term) alist)
+ (mv-nth 0 (simple-one-way-unify pat x alist)))
(equal (substitute-into-list
term (mv-nth 1 (simple-one-way-unify pat x alist)))
(substitute-into-list term alist)))
@@ -335,13 +342,15 @@
(defthm-simple-term-vars-flag
substitute-into-one-way-unify-lst-reduce-lemma
(simple-term-vars
- (implies (all-keys-bound (simple-term-vars term) alist)
+ (implies (and (all-keys-bound (simple-term-vars term) alist)
+ (mv-nth 0 (simple-one-way-unify-lst pat x alist)))
(equal (substitute-into-term
term (mv-nth 1 (simple-one-way-unify-lst pat x alist)))
(substitute-into-term term alist)))
:name substitute-into-one-way-unify-lst-reduce)
(simple-term-vars-lst
- (implies (all-keys-bound (simple-term-vars-lst term) alist)
+ (implies (and (all-keys-bound (simple-term-vars-lst term) alist)
+ (mv-nth 0 (simple-one-way-unify-lst pat x alist)))
(equal (substitute-into-list
term (mv-nth 1 (simple-one-way-unify-lst pat x alist)))
(substitute-into-list term alist)))
@@ -404,7 +413,7 @@
(equal (substitute-into-list pat subst) x)))
:name simple-one-way-unify-lst-correct)
:hints (("goal" :induct (simple-one-way-unify-flag flag pat x alist))))
-
+
(in-theory (disable simple-one-way-unify simple-one-way-unify-lst))
(defthm simple-one-way-unify-usage
@@ -434,7 +443,11 @@
(subst (mv-nth 1
(simple-one-way-unify-lst
template term
alist)))))
:in-theory (disable substitute-into-list-correct))))
-
+
+
+
+
+
#||