aboutsummaryrefslogtreecommitdiff
path: root/tests/stlc-pred.rkt
blob: f7afc43e9c197731b6661b10ece0dfc36195f3fb (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
#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)))