#lang typed/racket #:optimize

(provide head queue)


(define-type (Promiseof A) (Boxof (U (→ (Listof A)) (Listof A))))

;; Physicists Queue
;; Maintains invariant lenr <= lenf
;; pref is empty only if lenf = 0
(struct: (A) Queue ([preF  : (Listof A)]
                    [front : (Promiseof A)]
                    [lenf  : Integer]
                    [rear  : (Listof A)]
                    [lenr  : Integer]))

(define-syntax-rule (force promise)
  (let ([p (unbox promise)])
    (if (procedure? p)
        (let ([result (p)])
          (set-box! promise result)
          result)
        ; (error 'force "not a promise ~s" promise)
        p)))

;; Maintains "preF" invariant (preF in not not null when front is not null)
(: check-pref-inv : 
   (All (A) ((Listof A) (Promiseof A) Integer (Listof A) Integer ->
                        (Queue A))))
(define (check-pref-inv pref front lenf rear lenr)
  (if (null? pref)
      ((inst Queue A) (force front) front lenf rear lenr)
      (Queue pref front lenf rear lenr)))


;; Maintains lenr <= lenf invariant
(: check-len-inv : 
   (All (A) ((Listof A) (Promiseof A) Integer (Listof A) Integer -> (Queue A))))
(define (check-len-inv pref front lenf rear lenr)
  (if (>= lenf lenr)
      (check-pref-inv pref front lenf rear lenr)
      (let*: ([newpref : (Listof A) (force front)]
              [newf : (Promiseof A)
               (box (lambda () (append newpref (reverse rear))))])
        ((inst check-pref-inv A) newpref newf 
                                 (+ lenf lenr) null 0))))

;; Maintains queue invariants
(: internal-queue : 
   (All (A) ((Listof A) (Promiseof A) Integer (Listof A) Integer -> (Queue A))))
(define (internal-queue pref front lenf rear lenr)
  (check-len-inv pref front lenf rear lenr))

;; Enqueues an item into the list
(: enqueue : (All (A) (A (Queue A) -> (Queue A))))
(define (enqueue item que)
  (internal-queue (Queue-preF que)
                  (Queue-front que)
                  (Queue-lenf que)
                  (cons item (Queue-rear que))
                  (add1 (Queue-lenr que))))


;; Returns the first element in the queue if non empty. Else raises an error
(: head : (All (A) ((Queue A) -> A)))
(define (head que)
  (if (zero? (Queue-lenf que))
      (error 'head "given queue is empty")
      (car (Queue-preF que))))


;; Queue constructor function
(: queue : (All (A) (A * -> (Queue A))))
(define (queue . items)
  (foldl (inst enqueue A)
         ((inst Queue A) '() (box (lambda: () '())) 0 '() 0) items))