From 1ac1027c02e6ddb480d1db82a894ec3c9a974538 Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Wed, 19 Mar 2014 10:49:55 -0500
Subject: [PATCH] add tests to the poly-stlc model

---
 .../examples/benchmark/poly-stlc/tests.rkt    | 112 ++++++++++++++++++
 1 file changed, 112 insertions(+)
 create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt

diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt
new file mode 100644
index 0000000000..f3a780f955
--- /dev/null
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/tests.rkt
@@ -0,0 +1,112 @@
+#lang racket/base
+(require redex/reduction-semantics 
+         "poly-stlc-base.rkt")
+
+(test-equal (judgment-holds (typeof • 5 τ) τ)
+            (list (term int)))
+(test-equal (judgment-holds (typeof • [nil @ int] τ) τ)
+            (list (term (list int))))
+(test-equal (judgment-holds (typeof • ([cons @ int] 1) τ) τ)
+            (list (term ((list int) → (list int)))))
+(test-equal (judgment-holds (typeof • (([cons @ int] 1) [nil @ int]) τ) τ)
+            (list (term (list int))))
+(test-equal (judgment-holds (typeof • (λ (x int) x) τ) τ)
+            (list (term (int → int))))
+(test-equal (judgment-holds (typeof • (λ (x (int → int)) (λ (y int) x)) τ) τ)
+            (list (term ((int → int) → (int → (int → int))))))
+(test-equal (judgment-holds
+             (typeof •
+                     ([tl @ int]
+                      ([hd @ (list int)]
+                       ((λ (l (list (list int)))
+                          (([cons @ (list int)] (([cons @ int] 1) [nil @ int]))
+                           l))
+                        [nil @ (list int)])))
+                     τ)
+             τ)
+            (list (term (list int))))
+(test-equal (judgment-holds
+             (typeof •
+                     (([[map @ int] @ (list int)]
+                       (λ (x int) (([cons @ int] x) [nil @ int])))
+                      (([cons @ int] 2)
+                       (([cons @ int] 4)
+                        [nil @ int])))
+                     τ)
+             τ)
+            (list (term (list (list int)))))
+
+(test-->> red (term ((λ (x int) x) 7)) (term 7))
+(test-->> red (term (((λ (x int) (λ (x int) x)) 2) 1)) (term 1))
+(test-->> red (term (((λ (x int) (λ (y int) x)) 2) 1)) (term 2))
+(test-->> red 
+          (term ((λ (x int) (([cons @ int] x) [nil @ int])) 11))
+          (term (([cons @ int] 11) [nil @ int])))
+(test-->> red 
+          (term ((λ (x int) (([cons @ int] x) [nil @ int])) 11))
+          (term (([cons @ int] 11) [nil @ int])))
+(test-->> red 
+          (term (([cons @ int] ((λ (x int) x) 11)) [nil @ int]))
+          (term (([cons @ int] 11) [nil @ int])))
+(test-->> red
+          (term ([cons @ int] ((λ (x int) x) 1)))
+          (term ([cons @ int] 1)))
+(test-->> red
+          (term (([cons @ int] ((λ (x int) x) 1)) [nil @ int]))
+          (term (([cons @ int] 1) [nil @ int])))
+(test-->> red
+          (term ([hd @ int] ((λ (x int) (([cons @ int] x) [nil @ int])) 11)))
+          (term 11))
+(test-->> red
+          (term ([tl @ int] ((λ (x int) (([cons @ int] x) [nil @ int])) 11)))
+          (term [nil @ int]))
+(test-->> red
+          (term ([tl @ int] [nil @ int]))
+          "error")
+(test-->> red
+          (term ([hd @ int] [nil @ int]))
+          "error")
+(test-->> red
+          (term ((λ (f (int → (list int))) (f 3)) ([cons @ int] 1)))
+          (term (([cons @ int] 1) 3)))
+(test-->> red
+          (term 
+           ([tl @ int]
+            ([hd @ (list int)]
+             ((λ (l (list (list int)))
+                (([cons @ (list int)] (([cons @ int] 1) [nil @ int]))
+                 l))
+              [nil @ (list int)]))))
+          (term [nil @ int]))
+
+(test-->> red
+          (term (([[map @ int] @ (list int)]
+                  (λ (x int) (([cons @ int] x) [nil @ int])))
+                 (([cons @ int] 2)
+                  (([cons @ int] 4)
+                   [nil @ int]))))
+          (term (((cons @ (list int)) (((cons @ int) 2) (nil @ int)))
+                 (((cons @ (list int)) (((cons @ int) 4) (nil @ int)))
+                  (nil @ (list int))))))
+(test-equal (Eval (term ((λ (x int) x) 3)))
+            (term 3))
+
+
+
+#|
+;; tests for arithmetic; not yet added to the model.
+
+(test-equal (judgment-holds (typeof • ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
+            (list (term int)))
+(test-->> red
+          (term ((+ 1) ([hd @ int] [nil @ int])))
+          "error")
+(test-->> red
+          (term ((+ ((+ 1) 2)) ((+ 3) 4)))
+          (term 10))
+(test-->> red
+          (term ((λ (f (int → int)) (f 3)) (+ 1)))
+          (term 4))
+|#
+
+(test-results)