This version of the file also performs an in-place imperative quicksort... but using store-passing style!

qsort-store-passing-style.rkt

#lang plai-typed

#;(require rackunit)

(require (typed-in
          racket (round : (number -> number))))

;; let's implement quicksort. Using mutation.

;; a store is a map from numbers to numbers
(define-type-alias Sto (hashof number number))

(define empty-sto (hash empty))

;; a MuVec represents a mutable vector
(define-type MuVec
  [muvec (ptr : number) (len : number)])

;; example of vector
(vector 3 4 12)

#;(test (vec-swap (vector 3 4 12) 0 1)
      (vector 4 3 12))




;; fetch an element from the store
(define (fetch-from-sto [pointer : number] [store : Sto])
  (type-case (optionof number)(hash-ref store pointer)
    [some (n) n]
    [else (error 'fetch-from-sto (string-append "unallocated memory location: "
                                                (to-string pointer)))]))

(test (fetch-from-sto 3 (hash (list (values 2 1234) (values 3 9999) (values 10 19287))))
      9999)

;; mutate an element in the store
(define (update-sto [pointer : number] [new-val : number] [store : Sto])
  (hash-set store pointer new-val))

(test (update-sto 3  23 (hash (list (values 2 1234) (values 3 9999) (values 10 19287))))
      (hash (list (values 2 1234) (values 3 23) (values 10 19287))))


;; represent a pair of a muvec and a store
(define-type Vec*Sto
  [v*s (v : MuVec) (s : Sto)])

;; represent a pair of a number and a store
(define-type Num*Sto
  [n*s (n : number) (s : Sto)])

;; quicksort takes a mutable vector of numbers, and sorts them
;; destructively
(define (quicksort [vec : MuVec] [sto : Sto]) : Vec*Sto
  (let ([sto2 (qsort-helper vec 0 (muvec-len vec) sto)])
    (v*s vec sto2)))

;; qsort-helper takes a mutable vector of numbers and a start
;; and end index, and sorts the numbers in the range [start .. end).
;; it returns nothing.
(define (qsort-helper [vec : MuVec] [start : number] [end : number]
                      [sto : Sto]) : Sto
  (cond [(< (- end start) 2) sto]
        [else
         (local
           [(define pivot-posn (round (/ (+ start end) 2)))
            (define pivot-value (muvec-ref vec pivot-posn sto))
            (define first-larger-posn*sto2
              (do-qsort-loop-1 vec start (sub1 end) pivot-value
                               pivot-posn sto))
            (define first-larger-posn (n*s-n first-larger-posn*sto2))
            (define sto2 (n*s-s first-larger-posn*sto2))]
         ;; since the element before first-larger-posn
         ;; is known to be the pivot, we can shrink the recursive
         ;; call on the first half by at least one.
         (let ([sto3 (qsort-helper vec start (sub1 first-larger-posn)
                                   sto2)])
           (qsort-helper vec first-larger-posn end sto3)))]))

;; do-qsort-loop-1 takes an array and two array indexes and a
;; pivot value, and
;; scans for elements to be swapped, so that at the end
;; all of the elements <= the pivot are to the left of those
;; greater. it returns the smallest index such that all
;; lower indexes are known to be smaller than or equal to
;; the pivot.
;;
;; NB: the pivot value *must* occur in the range, or things
;; break.
;;
;; the invariant here is that the elements to the left of
;; the 'first' are known to be <= the pivot, and those to
;; the right of the 'last' are known to be larger than the
;; pivot.
;;
;; the 'progress' argument here involves induction on (last-first).
;; specifically, if (last-first) is less than zero, then both
;; of the following two functions halt. Otherwise, suppose
;; that the induction hypothesis holds for (last-first-1).
;; it turns out that we want to consider the second function first.
;; the second function can either halt, or it can decrease 'last',
;; which allows us to use the induction hypothesis, or it can perform
;; a swap and both increase first and reduce last, which uses the
;; induction hypothesis. This proves that the *second* helper function
;; always halts.
;; for the first function, it can either halt immediately, or it
;; can increase first (and then the induction hypothesis applies), or
;; it can make a call with the same value of (last-first) to the
;; second function, for which we've already proved the lemma. QED!
;; And: what a pain in the rear!
;;
;; painfully, we have a problem that we may wind up discovering
;; that all of the elements are <= the pivot, meaning that the
;; parent function is going to recur on a "sub-array" that is of
;; the same size. In order to ensure that the parent function makes
;; progress, we need to ensure that the pivot itself winds up
;; at a known location, so that we can guarantee that this element
;; won't be visited again. Blecch.
(define (do-qsort-loop-1 [vec : MuVec] [first : number] [last : number]
                         [pivot-value : number] [pivot-index : number]
                         [sto : Sto]) : Num*Sto
  (cond [(< last first)
         ;; ensure that the pivot is just before the split.
         (n*s first
              (vec-swap vec pivot-index (sub1 first) sto))]
        [(<= (muvec-ref vec first sto) pivot-value)
         (do-qsort-loop-1 vec (add1 first) last pivot-value pivot-index
                          sto)]
        [else ;; found an element that needs to be swapped
         (do-qsort-loop-2 vec first last pivot-value pivot-index
                          sto)]))

;; do-qsort-loop-2 does the "second half" of the qsort loop,
;; where we're scanning for an element to swap with the one
;; found by the first loop.
;;
;; the invariant here, along with the invariant from the prior
;; function, is that 'first' is known to point to an element
;; that is larger than the pivot.
(define (do-qsort-loop-2 [vec : MuVec] [first : number] [last : number]
                         [pivot-value : number] [pivot-index : number]
                         [sto : Sto]) : Num*Sto
  (cond [(< last first)
         (n*s
           first
           (vec-swap vec pivot-index (sub1 first) sto))]
        [(< pivot-value (muvec-ref vec last sto))
         (do-qsort-loop-2 vec first (sub1 last) pivot-value
                          pivot-index sto)]
        [else ;;found two elements that need to be swapped
           ;; they can't be the same, if the invariants hold.
         (let ([sto2 (vec-swap vec first last sto)])
           ;; oh no! if the newly swapped element is = to the pivot,
           ;; we need to know that:
           (local
             [(define new-pivot-index
                (cond [(= last pivot-index) first]
                      [else pivot-index]))]
             (do-qsort-loop-1 vec (add1 first) (sub1 last) pivot-value
                              new-pivot-index sto2)))]))

;; swap two elements in a mutable array
(define (vec-swap [vec : MuVec] [a : number] [b : number] [sto : Sto])
  : Sto
  (let ([tmp (muvec-ref vec a sto)])
    (let ([sto2 (muvec-set! vec a (muvec-ref vec b sto) sto)])
      (muvec-set! vec b tmp sto2))))

;; refer to an element of a muvec
(define (muvec-ref [muvec : MuVec] [index : number] [sto : Sto]) : number
  (fetch-from-sto (+ (muvec-ptr muvec) index) sto))

;; update an element of a muvec
(define (muvec-set! [muvec : MuVec] [index : number] [new-val : number]
                   [sto : Sto]) : Sto
  (update-sto (+ (muvec-ptr muvec) index) new-val sto))

(test
 (vec-swap (muvec 237 3) 0 1
           (hash (list (values 237 3) (values 238 4) (values 239 12))))
 (hash (list (values 237 4) (values 238 3) (values 239 12))))



;(test (do-qsort-loop-1 (vector 23 4 6 8 5 9 22) 1 5 9 5 empty-sto) 6)
;(test (do-qsort-loop-1 (vector 23 4 6 8 5 9 22) 1 5 5 4 empty-sto) 3)
;(test (do-qsort-loop-1 (vector 23 4 6 8 5 9 22) 1 5 4 1 empty-sto) 2)


(vector 4 12 3 19 12 5)

(test
 (quicksort (muvec 322 6)
            (hash (list (values 322 4)
                        (values 323 12)
                        (values 324 3)
                        (values 325 19)
                        (values 326 12)
                        (values 327 5))))
 (v*s (muvec 322 6)
      (hash (list (values 322 3)
                  (values 323 4)
                  (values 324 5)
                  (values 325 12)
                  (values 326 12)
                  (values 327 19)))))