From e09e442c418565dd076499df04e593ad54502889 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 31 Jan 2017 09:54:29 -0500 Subject: [PATCH] macrotypes/tests/fomega-tests passing --- macrotypes/examples/tests/fomega-tests.rkt | 233 +++++++++++---------- macrotypes/typecheck.rkt | 1 + 2 files changed, 128 insertions(+), 106 deletions(-) diff --git a/macrotypes/examples/tests/fomega-tests.rkt b/macrotypes/examples/tests/fomega-tests.rkt index 3abafe8..cb78ae8 100644 --- a/macrotypes/examples/tests/fomega-tests.rkt +++ b/macrotypes/examples/tests/fomega-tests.rkt @@ -98,118 +98,139 @@ ;(check-type Pair : (⇒ ★ ★ ★)) (check-type Pair :: (⇒ ★ ★ (∀★ ★))) -;; (check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X))) -;; ; parametric pair constructor -;; (check-type -;; (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) -;; : (∀ ([X : ★][Y : ★]) (→ X Y (tyapp Pair X Y)))) -;; ; concrete Pair Int String constructor -;; (check-type -;; (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) -;; Int String) -;; : (→ Int String (tyapp Pair Int String))) -;; ;; Pair Int String value -;; (check-type -;; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) -;; Int String) 1 "1") -;; : (tyapp Pair Int String)) -;; ;; fst: parametric -;; (check-type -;; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) -;; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) X))) -;; ;; fst: concrete Pair Int String accessor -;; (check-type -;; (inst -;; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) -;; Int String) -;; : (→ (tyapp Pair Int String) Int)) -;; ;; apply fst -;; (check-type -;; ((inst -;; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) -;; Int String) -;; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) -;; Int String) 1 "1")) -;; : Int ⇒ 1) -;; ;; snd -;; (check-type -;; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) -;; : (∀ ([X : ★][Y : ★]) (→ (tyapp Pair X Y) Y))) -;; (check-type -;; (inst -;; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) -;; Int String) -;; : (→ (tyapp Pair Int String) String)) -;; (check-type -;; ((inst -;; (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) -;; Int String) -;; ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) -;; Int String) 1 "1")) -;; : String ⇒ "1") +(check-type (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) x)) + : (∀ ([X :: ★][Y :: ★]) (→ X Y X))) +; parametric pair constructor +(check-type + (Λ ([X :: ★] [Y :: ★]) + (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) + : (∀ ([X :: ★][Y :: ★]) (→ X Y (tyapp Pair X Y)))) +; concrete Pair Int String constructor +(check-type + (inst (Λ ([X :: ★] [Y :: ★]) + (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) + Int String) + : (→ Int String (tyapp Pair Int String))) +;; Pair Int String value +(check-type + ((inst (Λ ([X :: ★] [Y :: ★]) + (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) + Int String) 1 "1") + : (tyapp Pair Int String)) +;; fst: parametric +(check-type + (Λ ([X :: ★][Y :: ★]) + (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) + ((inst p X) (λ ([x : X][y : Y]) x)))) + : (∀ ([X :: ★][Y :: ★]) (→ (tyapp Pair X Y) X))) +;; fst: concrete Pair Int String accessor +(check-type + (inst + (Λ ([X :: ★][Y :: ★]) + (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) + ((inst p X) (λ ([x : X][y : Y]) x)))) + Int String) + : (→ (tyapp Pair Int String) Int)) +;; apply fst +(check-type + ((inst + (Λ ([X :: ★][Y :: ★]) + (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) + ((inst p X) (λ ([x : X][y : Y]) x)))) + Int String) + ((inst (Λ ([X :: ★] [Y :: ★]) + (λ ([x : X] [y : Y]) + (Λ ([R :: ★]) + (λ ([p : (→ X Y R)]) (p x y))))) + Int String) 1 "1")) + : Int ⇒ 1) +;; snd +(check-type + (Λ ([X :: ★][Y :: ★]) + (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) + ((inst p Y) (λ ([x : X][y : Y]) y)))) + : (∀ ([X :: ★][Y :: ★]) (→ (tyapp Pair X Y) Y))) +(check-type + (inst + (Λ ([X :: ★][Y :: ★]) + (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) + ((inst p Y) (λ ([x : X][y : Y]) y)))) + Int String) + : (→ (tyapp Pair Int String) String)) +(check-type + ((inst + (Λ ([X :: ★][Y :: ★]) + (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) + ((inst p Y) (λ ([x : X][y : Y]) y)))) + Int String) + ((inst (Λ ([X :: ★] [Y :: ★]) + (λ ([x : X][y : Y]) + (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) + Int String) 1 "1")) + : String ⇒ "1") -;; ;; sysf tests wont work, unless augmented with kinds -;; (check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X))) +;; sysf tests wont work, unless augmented with kinds +(check-type (Λ ([X :: ★]) (λ ([x : X]) x)) : (∀ ([X :: ★]) (→ X X))) -;; (check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true -;; (check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false -;; (check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv +(check-type (Λ ([X :: ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X :: ★]) (→ X X X))) ; true +(check-type (Λ ([X :: ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X :: ★]) (→ X X X))) ; false +(check-type (Λ ([X :: ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y :: ★]) (→ Y Y Y))) ; false, alpha equiv -;; (check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) -;; : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2))))) +(check-type (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) + : (∀ ([t1 :: ★]) (∀ ([t2 :: ★]) (→ t1 (→ t2 t2))))) -;; (check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) -;; : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4))))) +(check-type (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) + : (∀ ([t3 :: ★]) (∀ ([t4 :: ★]) (→ t3 (→ t4 t4))))) -;; (check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) -;; : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4))))) +(check-not-type (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) + : (∀ ([t4 :: ★]) (∀ ([t3 :: ★]) (→ t3 (→ t4 t4))))) -;; (check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int)) -;; (check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int) -;; ; first inst should be discarded -;; (check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int)) -;; ; second inst is discarded -;; (check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int)) +(check-type (inst (Λ ([t :: ★]) (λ ([x : t]) x)) Int) : (→ Int Int)) +(check-type (inst (Λ ([t :: ★]) 1) (→ Int Int)) : Int) +; first inst should be discarded +(check-type (inst (inst (Λ ([t :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int)) +; second inst is discarded +(check-type (inst (inst (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int)) -;; ;; polymorphic arguments -;; (check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t))) -;; (check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s))) -;; (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t)))) -;; (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t)))) -;; (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s)))) -;; (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u)))) -;; (check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u)))) -;; (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x))) -;; (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1)) -;; (check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u))) -;; (check-type -;; (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int)) -;; (check-type -;; ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10) -;; : Int ⇒ 10) -;; (check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int))) -;; (check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int)) -;; (check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) -;; (Λ ([s : ★]) (λ ([y : s]) y))) -;; : Int ⇒ 10) +;; polymorphic arguments +(check-type (Λ ([t :: ★]) (λ ([x : t]) x)) : (∀ ([t :: ★]) (→ t t))) +(check-type (Λ ([t :: ★]) (λ ([x : t]) x)) : (∀ ([s :: ★]) (→ s s))) +(check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([s :: ★]) (∀ ([t :: ★]) (→ t t)))) +(check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([r :: ★]) (∀ ([t :: ★]) (→ t t)))) +(check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([r :: ★]) (∀ ([s :: ★]) (→ s s)))) +(check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([r :: ★]) (∀ ([u :: ★]) (→ u u)))) +(check-type (λ ([x : (∀ ([t :: ★]) (→ t t))]) x) : (→ (∀ ([s :: ★]) (→ s s)) (∀ ([u :: ★]) (→ u u)))) +(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x))) +(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1)) +(check-type ((λ ([x : (∀ ([t :: ★]) (→ t t))]) x) (Λ ([s :: ★]) (λ ([y : s]) y))) : (∀ ([u :: ★]) (→ u u))) +(check-type + (inst ((λ ([x : (∀ ([t :: ★]) (→ t t))]) x) (Λ ([s :: ★]) (λ ([y : s]) y))) Int) : (→ Int Int)) +(check-type + ((inst ((λ ([x : (∀ ([t :: ★]) (→ t t))]) x) (Λ ([s :: ★]) (λ ([y : s]) y))) Int) 10) + : Int ⇒ 10) +(check-type (λ ([x : (∀ ([t :: ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t :: ★]) (→ t t)) (→ Int Int))) +(check-type (λ ([x : (∀ ([t :: ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t :: ★]) (→ t t)) Int)) +(check-type ((λ ([x : (∀ ([t :: ★]) (→ t t))]) ((inst x Int) 10)) + (Λ ([s :: ★]) (λ ([y : s]) y))) + : Int ⇒ 10) -;; ;; previous tests ------------------------------------------------------------- -;; (check-type 1 : Int) -;; (check-not-type 1 : (→ Int Int)) -;; ;(typecheck-fail #f) ; unsupported literal -;; (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) -;; (check-not-type (λ ([x : Int]) x) : Int) -;; (check-type (λ ([x : Int]) x) : (→ Int Int)) -;; (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) -;; (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) -;; (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type -;; (typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type -;; (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type -;; (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) -;; : (→ (→ Int Int Int) Int Int Int)) -;; (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) -;; (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int -;; (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int -;; (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args -;; (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) +;; previous tests ------------------------------------------------------------- +(check-type 1 : Int) +(check-not-type 1 : (→ Int Int)) +;(typecheck-fail #f) ; unsupported literal +(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) +(check-not-type (λ ([x : Int]) x) : Int) +(check-type (λ ([x : Int]) x) : (→ Int Int)) +(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) +(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) +(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type +(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type +(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type +(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + : (→ (→ Int Int Int) Int Int Int)) +(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) +(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int +(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int +(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args +(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index a5185a4..240877f 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -660,6 +660,7 @@ [(~var _ id) (add-orig (syntax/loc stx τ-) stx)] ; defer to τ- error [(_ (~or (bv:id (... (... ...))) (~and (~fail #:unless #,(attribute has-annotations?)) + ([_ (~datum key2) _] (... (... ...))) bvs+ann)) . args) #:with bvs+ks (if #,(attribute has-annotations?)