aboutsummaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/stlc-imp.rkt29
-rw-r--r--tests/stlc-pred.rkt29
-rw-r--r--tests/stlc.rkt8
3 files changed, 4 insertions, 62 deletions
diff --git a/tests/stlc-imp.rkt b/tests/stlc-imp.rkt
deleted file mode 100644
index 44e0c17..0000000
--- a/tests/stlc-imp.rkt
+++ /dev/null
@@ -1,29 +0,0 @@
-#lang racket
-(require (except-in rackunit check))
-(require "../stlc-imp.rkt")
-
-(define-test-suite landins-knot
- (check-exn
- exn:fail?
- (λ () (infer '
- (let (id : (Nat → 1 Nat)) (λ x x)
- (let (r : (Ref (Nat → 0 Nat))) (new id)
- (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
- (set r f
- (f 0))))))))
-
- (check-eq? ; fixme: this should fail
- (infer '
- (let (id : (Nat → 0 Nat)) (λ x x)
- (let (r : (Ref (Nat → 0 Nat))) (new id)
- (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
- (f 0)))))
- 'Nat)
-
- (check-true
- (check '
- (let (id : (Nat → 0 Nat)) (λ x x)
- (let (r : (Ref (Nat → 0 Nat))) (new id)
- (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
- (f 0))))
- 'Nat)))
diff --git a/tests/stlc-pred.rkt b/tests/stlc-pred.rkt
deleted file mode 100644
index f7afc43..0000000
--- a/tests/stlc-pred.rkt
+++ /dev/null
@@ -1,29 +0,0 @@
-#lang racket
-(require (except-in rackunit check))
-(require "../stlc-pred.rkt")
-
-(define-test-suite landins-knot
- (check-exn
- exn:fail?
- (λ () (infer '
- (let (id : (Nat → 0 Nat)) (λ x x)
- (let (r : (Ref (Nat → 0 Nat))) (new id)
- (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
- (set r f
- (f 0))))))))
-
- (check-eq?
- (infer '
- (let (id : (Nat → 0 Nat)) (λ x x)
- (let (r : (Ref (Nat → 0 Nat))) (new id)
- (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
- (f 0)))))
- 'Nat)
-
- (check-true
- (check '
- (let (id : (Nat → 0 Nat)) (λ x x)
- (let (r : (Ref (Nat → 0 Nat))) (new id)
- (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
- (f 0))))
- 'Nat)))
diff --git a/tests/stlc.rkt b/tests/stlc.rkt
index 154e77d..cfec36f 100644
--- a/tests/stlc.rkt
+++ b/tests/stlc.rkt
@@ -2,7 +2,7 @@
(require (except-in rackunit check))
(require "../stlc.rkt")
-(check-equal? (interpret '(λ x x)) '(λ x x #hash()))
-(check-equal? (interpret '((λ a a) (x y))) '(x y))
-(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y))
-(check-equal? (interpret '((λ a (a y)) x)) '(x y))
+(check-equal? (interpret '(λ (x : Foo) x)) '(λ x x #hash()))
+(check-equal? (interpret '((λ (a : Bar) a) (x y))) '(x y))
+(check-equal? (interpret '((λ (a : Bat) (x y)) (λ (z : Bingus) z))) '(x y))
+(check-equal? (interpret '((λ (a : Baz) (a y)) x)) '(x y))