(module section-2-lump-embedding-tests mzscheme
  
  (require "section-2-lump-embedding.ss"
           "language-test-tools.ss"
           (lib "match.ss"))

  (provide tests)
  
  ;; fix : ((list -> num) -> list -> num) -> list -> num
  (define fix
    `(lambda (f)
       ((lambda (x) (f (lambda (z) ((x x) z))))
        (lambda (x) (f (lambda (z) ((x x) z)))))))
  
  ;; s->m : ty -> [L -> ty] term
  (define (s->m ty)
    (match ty
      [`num
        `(lambda (x : L)
           (MS num
               ((,fix
                  (lambda (s->mN)
                    (lambda (n)
                      (ifzero n
                              (SM num 0)
                              (SM num (+ 1 (MS num (s->mN (+ n -1)))))))))
                (SM L x))))]
      [`(,ty1 -> ,ty2)
        `(lambda (x : L)
           (lambda (y : ,ty1)
             (,(s->m ty2) (MS L ((SM L x) (,(m->s ty1) (SM ,ty1 y)))))))]))
  
  (define (m->s ty)
    (match ty
      [`num
        `(lambda (x)
           ((,fix
              (lambda (m->sN)
                (lambda (z)
                  (SM L 
                      (ifzero (MS num z)
                              (MS L 0)
                              (MS L (+ 1 (m->sN (SM num (+ (MS num z) -1)))))))))) 
            x))]
      [`(,ty1 -> ,ty2)
        `(lambda (x)
           (lambda (y)
             (,(m->s ty2) (SM ,ty2 ((MS (,ty1 -> ,ty2) x) (,(s->m ty1) (MS L y)))))))]))
  
  (define-tester test E)
  
  (define tests 
    (test-suite "lump embedding"
       (test-suite "basic operation"
          (test ((lambda (x : num) x) 4) 4)
          (test ((lambda (x : (num -> num)) x) (lambda (y : num) y))
                (lambda (y : num) y))
          (test (+ 5 12) 17)
          (test (- 12 5) 7)
          (test (- 5 12) 0)
          (test (ifzero 0 2 3) 2)
          (test (ifzero 1 2 3) 3))
       (test-suite "cross-boundary evaluation"
          (test (MS L (+ 5 12)) (MS L 17))
          (test (MS L (- 5 12)) (MS L 0))
          (test (MS L (ifzero 0 2 3)) (MS L 2))
          (test (MS L (ifzero 1 2 3)) (MS L 3))
          (test (MS L (nat? 12)) (MS L 0))
          (test (MS L (proc? 12)) (MS L 1))
          (test (MS L (proc? (lambda (x) x))) (MS L 0))
          (test (MS L (proc? 32)) (MS L 1))
          (test (MS L (ifzero (wrong "user-level error") 2 3)) "user-level error")
          (test (MS L (ifzero 0 (wrong "user-level error") 2)) "user-level error")
          (test (MS L (ifzero 1 (wrong "user-level error") 2)) (MS L 2))
          (test (MS num ((lambda (x) x) 4)) "Bad value"))
       (test-suite "cross-boundary typechecks and errors"
          (test ((lambda (x : (num -> num)) x) 4) "Type error")
          (test (MS L (SM L 3)) "Type error")
          (test (MS L (SM (num -> num)  ((lambda (x : num) x) (lambda (y : num) y)))) "Type error")
          (test (MS num (((lambda (x) (lambda (y) y)) (lambda (x) (x x))) (SM (num -> num) (lambda (z : (num -> num)) z))))
                "Type error")
          (test (MS num (SM num ((lambda (x : (num -> num)) (x 5)) (MS (num -> num) 5)))) "Bad value")
          (test (MS L ((SM (num -> num) (lambda (x : num) x)) (lambda (y) y))) "non-procedure"))
       (test-suite "cross-boundary operation"
          (test (MS num (SM num 1)) 1)
          (test ((lambda (x : num) (MS num (SM num x))) 2) 2)   
          (test (MS (num -> num) (SM (num -> num) (MS num 1))) "Type error")
          (test (MS L (SM num (MS (num -> num) 1))) "Type error")
          (test (MS L (SM num (MS num (lambda (x) 1)))) "Bad value")
          (test (MS L ((SM (num -> num) (MS (num -> num) (lambda (x) x))) 1)) "Bad value")
          (test (MS L ((SM (num -> num) (MS (num -> num) (lambda (x) x))) (lambda (x) x))) "Bad value")
          (test (MS L ((SM (num -> num) ((MS (num -> (num -> num)) (lambda (x) x)) 5)) 1)) "Bad value"))
       (test-suite "delumping"
          (test (,(s->m 'num) (MS L 3)) 3)
          (test (MS L (,(m->s 'num) (SM num 3))) (MS L 3))
          (test (((,(s->m `(num -> (num -> num))) (MS L (lambda (x) (lambda (y) x)))) 1) 2) 1)
          (test (((,(s->m `(num -> (num -> num))) (MS L (lambda (x) (lambda (y) y)))) 1) 2) 2)
          (test (((,(s->m `((num -> num) -> (num -> num))) 
                    (MS L (lambda (f) (lambda (x) (f (f x))))))
                  (lambda (x : num) (+ x 1)))
                 0)
                2)))))