(module section-3-natural-embedding-2-tests mzscheme
  (require "section-3-natural-embedding-2.ss"
           "language-test-tools.ss")
  (provide tests)
  
  (define-tester test (λ (t) (E (m:elaborate t))))

  (define tests
    (test-suite "separated-guards natural 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 "basic embedded program evaluation"
        (test (MS num (+ 5 12)) 17)
        (test (MS num (- 5 12)) 0)
        (test (MS num (ifzero 0 2 3)) 2)
        (test (MS num (ifzero 1 2 3)) 3)
        (test (MS num (nat? 12)) 0)
        (test (MS num (proc? 12)) 1)
        (test (MS num (proc? (lambda (x) x))) 0)
        (test (MS num (proc? 32)) 1)
        (test (MS num (ifzero (wrong "user-level error") 2 3)) "user-level error")
        (test (MS num (ifzero 0 (wrong "user-level error") 2)) "user-level error")
        (test (MS num (ifzero 1 (wrong "user-level error") 2)) 2))
      (test-suite "type tests"
        (test ((lambda (x : num) x) 4) 4)
        (test ((lambda (x : (num -> num)) x) 4) "Type error")
        (test ((lambda (x : num) x) (lambda (y : num) y)) "Type error")
        (test ((lambda (x : ((num -> num) -> (num -> num))) x) (lambda (y : (num -> num)) y))
              (lambda (y : num) y))
        (test (MS num ((lambda (x) x) 4)) 4)
        (test (((lambda (x : (num -> num)) (lambda (y : (num -> num)) y)) (lambda (x : num) x)) 
               (MS (num -> num) (lambda (z) (z z))))
              (lambda (y : num) (MS num ((lambda (y) (g num ((lambda (z) (z z)) (g num y)))) (SM num y)))))
        (test (MS num (SM num ((lambda (x : (num -> num)) (x 5)) (MS (num -> num) 5)))) "Non-procedure")
        (test (MS num ((SM (num -> num) (lambda (x : num) x)) (lambda (y) y))) "Non-number")
        (test (MS num (SM num 1)) 1)
        (test (MS (num -> num) (SM num 1)) "Non-procedure")
        (test (MS num (SM (num -> num) 1)) "Type error")
        (test (MS num (lambda (x) (SM num 1))) "Non-number")
        (test (MS (num -> num) (SM (num -> num) (lambda (x : num) x)))
              (lambda (y : num) 
                (MS num ((lambda (x) (g num ((lambda (y) (g num ((lambda (z) (SM num ((lambda (x : num) x) (MS num z))))
                                                                 (g num y))))
                                             (g num x))))
                         (SM num y)))))
        (test ((MS (num -> num) (SM (num -> num) (lambda (x : num) x))) 1) 1)
        (test (MS (num -> num) ((SM (num -> num) (lambda (x : num) x)) (lambda (x) x))) "Non-number")
        (test (MS num ((SM (num -> num) ((MS (num -> (num -> num)) (lambda (x) x)) 5)) 1)) "Non-procedure")))))