Freeze when opening certain files

[calebegg]

Freeze when opening certain files

[PeterReid]

This is the code that's making it hang, by the way.

(include-book "data-structures/structures" :dir :system)

(defstructure bst left key right)

(defun key< (x y)
  (< x y))
(in-theory (disable key<))

(defun key? (x)
  (natp x))
(in-theory (disable key?))

(defthm key-<-or->
  (implies (and (key? x)
                (key? y)
                (not (equal x y))
                (not (key< x y)))

           (key< y x))

  :hints (("Goal" :in-theory (enable key? key<))))

(defun bst-keys-below (x tr)
  (if (bst-p tr)
    (and (key< (bst-key tr) x)
         (bst-keys-below x (bst-left tr))
         (bst-keys-below x (bst-right tr)))
    t))
(defun bst-keys-above (x tr)
  (if (bst-p tr)
    (and (key< x (bst-key tr))
         (bst-keys-above x (bst-left tr))
         (bst-keys-above x (bst-right tr)))
    t))

(defun bst? (tr)
  (or (null tr)
      (and (bst-p tr)
           (key? (bst-key tr))
           (bst-keys-below (bst-key tr) (bst-left tr))
           (bst-keys-above (bst-key tr) (bst-right tr))
           (bst? (bst-left tr))
           (bst? (bst-right tr)))))


(defun bst-empty? (x)
  (null x))
(defun empty-bst ()
  nil)

(defthm left-<
  (implies (bst-p tr)
           (< (acl2-count (bst-left tr))
              (acl2-count tr)))
  :hints (("Goal" :in-theory (enable bst-left bst-p weak-bst-p))))
(defthm right-<
  (implies (bst-p tr)
           (< (acl2-count (bst-right tr))
              (acl2-count tr)))
  :hints (("Goal" :in-theory (enable bst-right bst-p weak-bst-p))))

(defun bst-insert (x tr)
  (if (bst-p tr)
    (cond ((key< x (bst-key tr))
           (bst (bst-insert x (bst-left tr))
                (bst-key tr)
                (bst-right tr)))
          ((key< (bst-key tr) x)
           (bst (bst-left tr)
                (bst-key tr)
                (bst-insert x (bst-right tr))))
          (t tr))
    (bst (empty-bst) x (empty-bst))))

(defthm left-<-root
  (implies (bst-left tr)
           (< (acl2-count (bst-left tr))
              (acl2-count tr)))
  :hints (("Goal"
           :in-theory (enable bst-left))))

(defthm right-<-root
  (implies (bst-right tr)
           (< (acl2-count (bst-right tr))
              (acl2-count tr)))
  :hints (("Goal"
           :in-theory (enable bst-right))))
(defun bst-first (tr)
  (if (bst-empty? (bst-left tr))
    (bst-key tr)
    (bst-first (bst-left tr))))

(defun bst-remove-first (tr)
  (if (bst-empty? (bst-left tr))
    (bst-right tr)
    (bst (bst-remove-first (bst-left tr))
         (bst-key tr)
         (bst-right tr))))

(defun bst-delete (x tr)
  (if (bst-p tr)
    (cond ((key< x (bst-key tr))
           (bst (bst-delete x (bst-left tr))
                (bst-key tr)
                (bst-right tr)))
          ((key< (bst-key tr) x)
           (bst (bst-left tr)
                (bst-key tr)
                (bst-delete x (bst-right tr))))
          ((equal (bst-key tr) x)
           (if (bst-empty? (bst-right tr))
             (bst-left tr)
             (bst (bst-left tr)
                  (bst-first (bst-right tr))
                  (bst-remove-first (bst-right tr))))
             ))
    (empty-bst)))

(defun bst-contains (x tr)
  (and (bst-p tr)
       (cond  ((key< x (bst-key tr))
               (bst-contains x (bst-left tr)))
              ((key< (bst-key tr) x)
               (bst-contains x (bst-right tr)))
              (t
               (equal (bst-key tr) x)))))


(defthm not-x-key<-x
  (implies (key? x)
           (not (key< x x)))
  :hints (("Goal" :in-theory (enable key? key<))))

(defthm contains-after-insert
  (implies (and (bst? tr)
                (key? x))
           (bst-contains x (bst-insert x tr)))
  :hints (("Goal"
           :use (:instance key-<-or-> (x x) (y (bst-key tr))))))

(defthm bst-keys-below-after-insert
  (implies (and (bst? tr)
                (key? x)
                (key? top)
                (bst-keys-below top tr)
                (key< x top))
           (bst-keys-below top (bst-insert x tr))))
(defthm bst-keys-above-after-insert
  (implies (and (bst? tr)
                (key? x)
                (key? bottom)
                (bst-keys-above bottom tr)
                (key< bottom x))
           (bst-keys-above bottom (bst-insert x tr))))

(defthm bst-after-insert
  (implies (and (bst? tr)
                (key? x))
           (bst? (bst-insert x tr))))

(defthm still-contains-after-insert 
  (implies (and (bst? tr)
                (key? x)
                (key? y)
                (bst-contains y tr))
           (bst-contains y (bst-insert x tr))))

(defthm not-contains-if-keys-above
  (implies (and (bst? tr)
                (key? x)
                (bst-keys-below x tr))
           (not (bst-contains x tr))))

(defthm not-contains-if-keys-below
  (implies (and (bst? tr)
                (key? x)
                (bst-keys-above x tr))
           (not (bst-contains x tr))))

(defthm not-<-and->
  (implies (and (key? x)
                (key? y)
                (key< x y))
           (not (key< y x)))
  :hints (("Goal" :in-theory (enable key? key<))))

;(defthm bst-p-if-exists
;  (implies (and (bst? tr)
;                (bst-left (bst-left tr)))
;           (bst-p (bst-left (bst-left tr)))))

(defthm key-<-transitive
  (implies (and (key? x) (key? y) (key? z)
                (key< x y) (key< y z))
           (key< x z))
  :hints (("Goal" :in-theory (enable key< key?))))

(defthm bst-first-is-key
  (implies (and (bst? tr)
                (bst-p tr))
           (key? (bst-first tr))))

(defthm bst-first-<-root
  (implies (and (bst? tr)
                (bst-p (bst-left tr)))
           (key< (bst-first tr)
                 (bst-key tr)))
  :hints (("Subgoal *1/2"
           :use (:instance key-<-transitive
                 (x (bst-first (bst-left tr)))
                 (y (bst-key (bst-left tr)))
                 (z (bst-key tr))))))

#|(defthm bst-root-not-<-bst-first
  (implies (and (bst? tr)
                (bst-p tr))
           (not (key< (bst-key tr)
                      (bst-first tr))))
  :hints (("Goal"
           :in-theory (disable key-<-transitive)

           :use (:instance key-<-transitive
                 (x (bst-first (bst-left tr)))
                 (y (bst-key (bst-left tr)))
                 (z (bst-key tr))))))
(defthm contains-first
  (implies (and (bst-p tr)
                (bst? tr))
           (bst-contains (bst-first tr) tr))
  :hints (("Subgoal *1/4"
           :use ((:instance key-<-transitive
                  (x (bst-first (bst-left tr)))
                  (y (bst-key (bst-left tr)))
                  (z (bst-key tr)))
                 (:instance bst-first-is-key
                  (tr (bst-left tr))
                  )
                 (:instance bst-first-<-root
                  (tr (bst-left tr)))))
          ("Subgoal *1/6"
           :use ((:instance key-<-transitive
                  (x (bst-first (bst-left tr)))
                  (y (bst-key (bst-left tr)))
                  (z (bst-key tr)))))))
|#

(defaxiom contains-first
  (implies (and (bst-p tr)
                (bst? tr))
           (bst-contains (bst-first tr) tr)))#|ACL2s-ToDo-Line|#


(defthm still-not-contains-after-remove-first
  (implies (and (bst? tr)
                (key? x)

                )
           (equal (bst-contains x (bst-remove-first tr))
                  (and (not (equal x (bst-first tr)))
                       (bst-contains x tr)))))

(defthm gone-after-delete
  (implies (and (bst? tr)
                (key? x))
           (not (bst-contains x (bst-delete x tr)))))

[calebegg]

I think this is fixed. flush() is on a different thread, at any rate, so if that was indeed the problem then it's fixed.