;; ---------------------------------------------------------------------------
;; ~/events/stack.events
;; ---------------------------------------------------------------------------

;; This file implements a generic data type stack.

(enable-theory lists)

;; I will use a shell for implementing the basic stack. The bottom element is
;; EmptyStack, stackp is the recognizer, push the constructor and 
;; top and pop the destructors.

(add-shell push EmptyStack is-stack
     ((top (none-of) zero)
      (pop (one-of is-stack) EmptyStack)))

;; The function to test for bottom element equality

(defn is-empty (s) 
  (if (is-stack s)
      (equal s (EmptyStack))
      F))

;; The functions for popping or pushing more than one element at a time.

(defn pop-n (n s)
 (if (not (is-stack s))
     s
     (if (zerop n)
	 s
	 (pop-n (sub1 n) (pop s)))))

(prove-lemma pop-n-emptystack (rewrite)
 (implies (numberp size)
	  (equal (pop-n size (emptystack))
		 (emptystack))))

;; The function top-n returns the top n elements of the stack in reverse order.

(defn top-n (n s)
 (if (or (not (is-stack s))
	 (equal s (emptystack)))
     nil
     (if (zerop n)
	 nil
         (append (top-n (sub1 n) (pop s))
		 (list (top s))))))

;; This function returns the number of elements on a stack.

(defn stack-length (s) 
  (if (or (not (is-stack s))
	  (is-empty s))
      0
      (add1 (stack-length (pop s)))))

;; This is a minor lemma to prove that a non-empty stack has non-zero length.

(prove-lemma not-empty-not-zero (rewrite)
 (implies (and (is-stack stack)
	       (not (is-empty stack)))
	  (lessp 0 (stack-length stack))))

;; Reading the stack from the bottom, i.e. the top element is last and 
;; the bottom element is first.  Note that (not (is-stack s)) was necessary 
;; for the proof of termination of this function. And I had to use append 
;; and put the second parameter in a list in order to obtain the function I
;; expected to have specified.

(defn from-bottom (s) 
   (if (or (is-empty s)
	   (not (is-stack s)))
       nil
       (append (from-bottom (pop s)) (list (top s)))))

;; One needs to know that pop is smaller than the original for a measure.

(prove-lemma lessp-pop-stack (rewrite)
  (implies (and (is-stack s)
		(not (is-empty s)))
	   (lessp (stack-length (pop s)) (stack-length s))))

;; This theorem is needed for the parser proof.

(prove-lemma append-from-bottom-pop-n (rewrite)
 (implies (is-stack s)
	  (equal (append (from-bottom (pop-n n s))
			 (top-n n s))
		 (from-bottom s))))

(prove-lemma plistp-from-bottom (rewrite)
 (implies (is-stack s)
	  (plistp (from-bottom s))))
       
(prove-lemma from-bottom-push (rewrite)
 (implies (is-stack b)
	  (equal (from-bottom (push a b))
		 (append (from-bottom b) (list a)))))

(deftheory stacks 
 (LESSP-POP-STACK FROM-BOTTOM NOT-EMPTY-NOT-ZERO STACK-LENGTH
  TOP-N POP-N pop-n-emptystack IS-EMPTY PUSH APPEND-FROM-BOTTOM-POP-N
  PLISTP-FROM-BOTTOM FROM-BOTTOM-PUSH))
(disable-theory stacks)
(disable-theory lists)