;;; $Id: set-ops-as-vector.scm,v 1.6 2005/03/28 19:32:54 dorn Exp $

;;; The following implements the set operations using vectors as the
;;; representation.

(module set-ops-as-vector (lib "typedscm.ss" "lib342")

(provide the-empty-set set-empty? set-size set set-member?
	set-one-elem set-rest set-subset? set-equal? set-add set-remove
	set-union set-minus set-intersect set-union-list set-union*)

(deftype the-empty-set (forall (T) (set-of T)))
(deftype set-empty? (forall (T) (-> ((set-of T)) boolean)))
(deftype set-size (forall (T) (-> ((set-of T)) number)))
(deftype set (forall (T) (-> (T ...) (set-of T))))
(deftype set-member? (forall (T) (-> (T (set-of T)) boolean)))
(deftype set-one-elem (forall (T) (-> ((set-of T)) T)))
(deftype set-rest (forall (T) (-> ((set-of T)) (set-of T))))
(deftype set-subset? (forall (T) (-> ((set-of T) (set-of T)) boolean)))
(deftype set-equal? (forall (T) (-> ((set-of T) (set-of T)) boolean)))
(deftype set-add (forall (T) (-> (T (set-of T)) (set-of T))))
(deftype set-remove (forall (T) (-> (T (set-of T)) (set-of T))))
(deftype set-union (forall (T) (-> ((set-of T) (set-of T)) (set-of T))))
(deftype set-minus (forall (T) (-> ((set-of T) (set-of T)) (set-of T))))
(deftype set-intersect (forall (T) (-> ((set-of T) (set-of T)) (set-of T))))
(deftype set-union-list (forall (T) (-> ((list-of (set-of T))) (set-of T))))
(deftype set-union* (forall (T) (-> ((set-of T) ...) (set-of T))))

(require (lib "vector-generator.scm" "lib342"))
;; In this file, sets are represented by vectors.
;; The vector contains no duplicates, and has no unused elements.
;; Hence the length of the vector is the size of the set.
(defrep (forall (T) (set-of T) (vector-of T)))

(define the-empty-set '#())

(define set-empty?
  (lambda (s)
    ;; ENSURES: result is true just when s is empty
    (zero? (vector-length s))))

(define set-size
  (lambda (s)
    ;; ENSURES: result is the number of elements in s
    (vector-length s)))

(define set
  (lambda args
    ;; ENSURES: result is a set containing just the elements in args
    (letrec ((squeeze-out-dups
	      (has-type
		(forall (T) (-> ((list-of T)) (list-of T)))
		(lambda (ls)
		  (if (null? ls)
		      '()
		      (if (member (car ls) (cdr ls))
			  (squeeze-out-dups (cdr ls))
			  (cons (car ls) (squeeze-out-dups (cdr ls)))))))))
      (list->vector (squeeze-out-dups args)))))

(define set-member?
  (lambda (e S)
    ;; ENSURES: result is true just when e is equal? to some element of S
    (not (negative? (set-ops:index-of e S)))))

(deftype set-ops:index-of
  (forall (T) (-> (T (vector-of T)) number)))
(define set-ops:index-of
  (lambda (e S)
    ;; REQUIRES: e occurs at most once in S
    ;; ENSURES: result is -1 if e does not occur in S,
    ;;          otherwise result is the index of e in S
    (letrec ((loop
	      (has-type
		(-> (number) number)
		  (lambda (i)
		    (if (or (negative? i) (equal? e (vector-ref S i)))
			i
			(loop (- i 1)))))))
	(loop (- (vector-length S) 1)))))

(define set-one-elem
  (lambda (s)
    ;; REQUIRES: s is not empty
    ;; ENSURES: result is a member of s
    (vector-ref s 0)))

(define set-rest 
  (lambda (s)
    ;; REQUIRES: s is not empty
    ;; ENSURES: result is the largest subset of s that does not contain
    ;;          the element (set-one-elem s)
    (list->vector (cdr (vector->list s)))))

(define set-subset?
  (lambda (S1 S2)
    ;; ENSURES: result is true just when S1 is a subset of S2,
    ;;          or equal to S2.  Membership is determined by equal?
    (letrec ((loop
	      (has-type
		(-> (number) boolean)
		(lambda (i)
		  (or (negative? i)
		      (and (set-member? (vector-ref S1 i) S2)
			   (loop (- i 1))))))))
      (loop (- (vector-length S1) 1)))))

(define set-equal?
  (lambda (S1 S2)
    ;; ENSURES: result is true just when S1 and S2 contain
    ;;          the same elements. Membership is determined by equal?
    (and (set-subset? S1 S2)
	 (set-subset? S2 S1))))

(define set-add			        
  (lambda (e S)
    ;; ENSURES: result contains the elements of S and also e
    (if (set-member? e S)
	S
	(list->vector (cons e (vector->list S))))))

(define set-remove			
  (lambda (e S)
    ;; ENSURES: result contains the elements of S except for e
    (let ((i (set-ops:index-of e S)))
      (if (negative? i)
	  S
	  ((vector-generator
	    (lambda (n)
	      (if (< n i)
		  (vector-ref S n)
		  (vector-ref S (+ n 1)))))
	   (- (vector-length S) 1))))))

(define set-union
  (lambda (S1 S2)
    ;; ENSURES: result contains the elements of both S1 and S2,
    ;; so that an element is a member if it's a member of either S1 or S2.
    (let ((S1-without-S2 (set-minus S1 S2)))
      (list->vector (append (vector->list S1-without-S2) (vector->list S2))))))

(define set-minus			
  (lambda (S1 S2)
    ;; ENSURES: result contains just the elements of S1 that are NOT in S2
    (letrec ((loop
	      (lambda (i S1)
		(if (negative? i)
		    S1
		    (loop (- i 1) (set-remove (vector-ref S2 i) S1))))))
      (loop (- (vector-length S2) 1) S1))))

(define set-intersect			
  (lambda (S1 S2)
    ;; ENSURES: result contains just the elements in both S1 AND S2
    (letrec ((common-members
	      (has-type
		(forall (T) (-> (number (list-of T)) (list-of T)))
		(lambda (i ls)
		  (if (negative? i)
		      ls
		      (common-members
		       (- i 1)
		       (if (set-member? (vector-ref S1 i) S2)
			   (cons (vector-ref S1 i) ls)
			   ls)))))))
      (list->vector (common-members (- (vector-length S1) 1) '())))))

(define set-union-list
  (lambda (lset)
    ;; ENSURES: result is the union of all the sets in lset.
    (if (null? lset)
	the-empty-set
	(set-union (car lset)
		   (set-union-list (cdr lset))))))

(define set-union*
  (lambda lset
    ;; ENSURES: result is the union of all the sets in lset.
    (set-union-list lset)))

) ; end module