diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/stlc-imp.rkt | 29 | ||||
-rw-r--r-- | tests/stlc-pred.rkt | 29 | ||||
-rw-r--r-- | tests/stlc.rkt | 8 |
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)) |