(module section-5-polymorphism-tests mzscheme

  (require "section-5-polymorphism.ss"
           "language-test-tools.ss")
  (provide tests)

  (define-tester test E)
  
  (define church4 '(LAMBDA (a) (lambda (f : (a -> a)) (lambda (x : a) (f (f (f (f x))))))))
  (define church-type '(forall (a) ((a -> a) -> (a -> a))))
  
  (define tests
    (test-suite "polymorphism tests"
      (test-suite "basic polymorphism tests"
        (test ((tyapp (LAMBDA (a) (lambda (x : a) x)) num) 3) 3)
        (test ((tyapp (LAMBDA (a) (lambda (x : a) (+ x 1))) num) 3) "Type error")
        (test (((tyapp ,church4 num) (lambda (x : num) (+ x 1))) 0) 4))
      (test-suite "ffi polymorphism tests"
        (test (MSG num ((GSM (forall (a) (a -> a)) (LAMBDA (a) (lambda (x : a) x))) 2)) 2)
        (test (MSG num (((GSM ,church-type ,church4) (lambda (x) (+ x 1))) 0)) 4)
        (test ((lambda (F : (forall (a) (a -> a)))
                 (((tyapp F (num -> num)) (lambda (x : num) x))
                  ((tyapp F num) 2)))
               (MSG (forall (a) (a -> a)) (lambda (x) x)))
              2)
        
        ;; this test shows that parametricity breaks in this particular scheme
        (test ((lambda (F : (forall (a) (a -> a)))
                 (((tyapp F (num -> num)) (lambda (x : num) x))
                  ((tyapp F num) 2)))
               (MSG (forall (a) (a -> a)) 
                    (lambda (x) (ifzero (nat? x) (+ x 1) x))))
              3)
        (test ((lambda (F : (forall (a) (a -> a)))
                 (((tyapp F (num -> num)) (lambda (x : num) x))
                  ((tyapp F num) 2)))
               (MSG (forall (a) (a -> a)) (lambda (x) 2)))
              "Non-procedure")))))