;; The gradually typed lambda calculus of:
;;
;; @InProceedings{ Siek06:gradual,
;;     author = {Jeremy G. Siek and Walid Taha},
;;     title = {Gradual typing for functional languages},
;;     booktitle = {Scheme and Functional Programming Workshop},
;;     year = 2006,
;;     month = {September} }
;;
;; and the space-efficient gradually typed lambda calculus of:
;;
;; @InProceedings{ Herman07:gradual,
;;     author = {David Herman and Aaron Tomb and Cormac Flanagan},
;;     title = {Space-Efficient Gradual Typing},
;;     booktitle = {Trends in Functional Programming},
;;     year = 2007,
;;     month = {April} }
;;
;; Usage:
;;    (pretty (cast-growth-example n))  ; pretty-prints a reduction sequence
;;    (gui (cast-growth-example n))     ; shows a reduction sequence graphically

(module lambda-gradual mzscheme
  (require "siek-taha.ss"
           "herman-tomb-flanagan.ss"
           (all-except "front-end.ss" next)
           (rename "front-end.ss" front-end:next next)
           "text-ui.ss")

  (define (next s x)
    (front-end:next (semantics-reduction-relation s) x))

  ;; ===========================================================================
  ;; EXAMPLES
  ;; ===========================================================================

  (define omega
    '(let (D : (dynamic -> dynamic) = (lambda (x : (dynamic -> dynamic))
                                        (x x)))
       (D D)))
     
  (define untyped-example
    '((lambda (x) x)
      ((lambda (y) y)
       (lambda (z) z))))

  (define typed-example
    '((lambda (x : int)
        (if #t (+ x 1) (- x 1)))
      42))

  (define cormacs-example
    '(let (Y = (lambda (f)
                 ((lambda (x)
                    (f (lambda (y) ((x x) y))))
                  (lambda (x)
                    (f (lambda (y) ((x x) y)))))))
       (let (fix : (((int -> int) -> (int -> int)) -> (int -> int)) = Y)
         (let (count = (fix (lambda (c : (int -> int))
                              (lambda (n : int)
                                (if (= n 0)
                                    0
                                    (+ 1 (c (- n 1))))))))
           (count 10)))))

  (define even/odd
    '(letrec ([even? : (int -> bool) = (lambda (n : int)
                                         (if (= n 0) #t (odd? (- n 1))))]
              [odd? : (int -> bool) = (lambda (n : int)
                                        (if (= n 0) #f (odd? (- n 1))))])
       (even? 0)))

  (define (tail-recursion-example size)
    `(letrec ([even? = (lambda (n : int)
                         (if (= n 0) #t (odd? (- n 1))))]
              [odd? : (int -> bool) =
                    (lambda (n : int)
                      (if (= n 0) #f (even? (- n 1))))])
       (even? ,size)))

  (define (cast-growth-example size)
    `(letrec ([even : (int -> ((dynamic -> dynamic) -> dynamic)) =
                    (lambda (n : int)
                      (lambda (f : (dynamic -> dynamic))
                        (if (= n 0)
                            (f #t)
                            ((odd (- n 1)) f))))]
              [odd : (int -> ((bool -> bool) -> bool)) =
                   (lambda (n : int)
                     (lambda (f : (bool -> bool))
                       (if (= n 0)
                           (f #f)
                           ((even (- n 1)) f))))])
       ((even ,size) (lambda (b : bool) #t))))

  ;; Example inspired by Section 2.2 (page 3) of:
  ;;
  ;; @InProceedings{ Minamide98:unboxing,
  ;;     author = {Yasuhiko Minamide and Jacques Garrigue},
  ;;     title = {On the Runtime Complexity of Type-Directed Unboxing},
  ;;     booktitle = {International Conference on Functional Programming},
  ;;     year = 1998,
  ;;     month = {September} }
  ;;
  ;; fun id (x:Dyn) : Dyn = x
  ;;
  ;; fun iter (f:Int -> Int) (n:Int) : Int =
  ;;     if n = 0
  ;;     then 0
  ;;     else f (iter (id f) (n - 1))
  ;;
  ;; iter (fn (n : Int) => n + 1) n
  (define (time-complexity-example size)
    `(letrec ([id : (dynamic -> dynamic) =
                  (lambda (x : dynamic) x)]
              [iter : ((int -> int) -> (int -> int)) =
                    (lambda (f : (int -> int))
                      (lambda (n : int)
                        (if (= n 0)
                            0
                            (f ((iter (id f)) (- n 1))))))])
       ((iter (lambda (n : int)
                (+ n 1)))
        ,size)))

  (provide (all-defined)
           semantics?
           st htf
           type-check
           count trace pretty))