copy over the rest of the non-mlish tests
This commit is contained in:
AlexKnauth
parent
a8f1634baa
commit
7677a6de28
|
|
@ -22,26 +22,25 @@
|
|||
(⊢ e- : ∃τ.norm)])
|
||||
|
||||
(define-typed-syntax open #:datum-literals (<=)
|
||||
[(open ([(tv:id x:id) <= e_packed]) e)
|
||||
#:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
|
||||
[(open [x:id <= e_packed with X:id] e)
|
||||
;; The subst below appears to be a hack, but it's not really.
|
||||
;; It's the (TaPL) type rule itself that is fast and loose.
|
||||
;; Leveraging the macro system's management of binding reveals this.
|
||||
;;
|
||||
;; Specifically, here is the TaPL Unpack type rule, fig24-1, p366:
|
||||
;; Γ ⊢ t_1 : {∃X,T_12}
|
||||
;; Γ,X,x:T_12 ⊢ t_2 : T_2
|
||||
;; Γ ⊢ e_packed : {∃X,τ_body}
|
||||
;; Γ,X,x:τ_body ⊢ e : τ_e
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X,x}=t_1 in t_2 : T_2
|
||||
;; Γ ⊢ (open [x <= e_packed with X] e) : τ_e
|
||||
;;
|
||||
;; There's *two* separate binders, the ∃ and the let,
|
||||
;; which the rule conflates.
|
||||
;;
|
||||
;; Here's the rule rewritten to distinguish the two binding positions:
|
||||
;; Γ ⊢ t_1 : {∃X_1,T_12}
|
||||
;; Γ,X_???,x:T_12 ⊢ t_2 : T_2
|
||||
;; Γ ⊢ e_packed : {∃X_1,τ_body}
|
||||
;; Γ,X_???,x:τ_body ⊢ e : τ_e
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
|
||||
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
|
||||
;;
|
||||
;; The X_1 binds references to X in T_12.
|
||||
;; The X_2 binds references to X in t_2.
|
||||
|
|
@ -49,26 +48,28 @@
|
|||
;;
|
||||
;; A first guess might be to replace X_??? with both X_1 and X_2,
|
||||
;; so all the potentially referenced type vars are bound.
|
||||
;; Γ ⊢ t_1 : {∃X_1,T_12}
|
||||
;; Γ,X_1,X_2,x:T_12 ⊢ t_2 : T_2
|
||||
;; Γ ⊢ e_packed : {∃X_1,τ_body}
|
||||
;; Γ,X_1,X_2,x:τ_body ⊢ e : τ_e
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
|
||||
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
|
||||
;;
|
||||
;; But this example demonstrates that the rule above doesnt work:
|
||||
;; (open ([x : X_2 (pack (Int 0) as (∃ (X_1) X_1))])
|
||||
;; (open [x <= (pack (Int 0) as (∃ (X_1) X_1)) with X_2]
|
||||
;; ((λ ([y : X_2]) y) x)
|
||||
;; Here, x has type X_1, y has type X_2, but they should be the same thing,
|
||||
;; so we need to replace all X_1's with X_2
|
||||
;;
|
||||
;; Here's the fixed rule, which is implemented here
|
||||
;;
|
||||
;; Γ ⊢ t_1 : {∃X_1,T_12}
|
||||
;; Γ,X_2,x:[X_2/X_1]T_12 ⊢ t_2 : T_2
|
||||
;; Γ ⊢ e_packed : {∃X_1,τ_body}
|
||||
;; Γ,X_2:#%type,x:[X_2/X_1]τ_body ⊢ e : τ_e
|
||||
;; ------------------------------
|
||||
;; Γ ⊢ let {X_2,x}=t_1 in t_2 : T_2
|
||||
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
|
||||
;;
|
||||
#:with [_ (x-) (e-) (τ_e)]
|
||||
#:with [e_packed- (~∃ (Y) τ_body)] (infer+erase #'e_packed)
|
||||
#:with τ_x (subst #'X #'Y #'τ_body)
|
||||
#:with [(X-) (x-) (e-) (τ_e)]
|
||||
(infer #'(e)
|
||||
#:tvctx #'([tv : #%type])
|
||||
#:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
|
||||
#:tvctx #'([X : #%type])
|
||||
#:ctx #`([x : τ_x]))
|
||||
(⊢ (let- ([x- e_packed-]) e-) : τ_e)])
|
||||
|
|
|
|||
|
|
@ -89,14 +89,14 @@
|
|||
|
||||
(define-typed-syntax inst
|
||||
[(inst e τ ...)
|
||||
#:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
|
||||
#:with [e- τ_e] (infer+erase #'e)
|
||||
#:with (~∀ (tv ...) τ_body) #'τ_e
|
||||
#:with (~∀★ k ...) (typeof #'τ_e)
|
||||
#:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
|
||||
#:when (stx-andmap
|
||||
(λ (t k) (or ((current-kind?) k)
|
||||
(type-error #:src t #:msg "not a valid type: ~a" t)))
|
||||
#'(τ ...) #'(k_τ ...))
|
||||
#:when (typechecks? #'(k_τ ...) #'(k ...))
|
||||
(⊢ e- : #,(substs #'(τ- ...) #'(tv ...) #'τ_body))])
|
||||
#:fail-unless (typechecks? #'(k_τ ...) #'(k ...))
|
||||
(typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...))
|
||||
#:with τ_inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
|
||||
(⊢ e- : τ_inst)])
|
||||
|
||||
;; TODO: merge with regular λ and app?
|
||||
;; - see fomega2.rkt
|
||||
|
|
|
|||
|
|
@ -16,14 +16,11 @@
|
|||
|
||||
(define-typed-syntax Λ
|
||||
[(Λ (tv:id ...) e)
|
||||
#:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
|
||||
#:with [(tv- ...) e- τ] (infer/tyctx+erase #'([tv : #%type] ...) #'e)
|
||||
(⊢ e- : (∀ (tv- ...) τ))])
|
||||
(define-typed-syntax inst
|
||||
[(inst e τ:type ...)
|
||||
#:with (e- (tvs (τ_body))) (⇑ e as ∀)
|
||||
;#:with [e- (~and t (~∀ tvs τ_body))] (infer+erase #'e)
|
||||
;#:with (_ Xs τ_orig) (get-orig #'t) ; doesnt work with implicit lifted→
|
||||
;#:with new-orig (substs #'(τ ...) #'Xs #'τ_orig)
|
||||
;(⊢ e- : #,(add-orig (substs #'(τ.norm ...) #'tvs #'τ_body) #'new-orig))]
|
||||
(⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))]
|
||||
[(_ e) #'e])
|
||||
#:with [e- (~∀ tvs τ_body)] (infer+erase #'e)
|
||||
#:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body)
|
||||
(⊢ e- : τ_inst)]
|
||||
[(inst e) #'e])
|
||||
|
|
|
|||
370
macrotypes/examples/tests/exist-tests.rkt
Normal file
370
macrotypes/examples/tests/exist-tests.rkt
Normal file
|
|
@ -0,0 +1,370 @@
|
|||
#lang s-exp "../exist.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X))
|
||||
(check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y))
|
||||
(typecheck-fail (pack (Int 0) as (∃ (X) Y)))
|
||||
(check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
|
||||
(typecheck-fail (pack (Int #t) as (∃ (X) X)))
|
||||
|
||||
(check-type (pack (Int (pack (Int 0) as (∃ (X) X))) as (∃ (Y) (∃ (X) X)))
|
||||
: (∃ (Y) (∃ (X) X)))
|
||||
(check-type (pack (Int +) as (∃ (X) (→ X Int Int))) : (∃ (X) (→ X Int Int)))
|
||||
(check-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
|
||||
as (∃ (Y) (∃ (X) (→ X Y Int))))
|
||||
: (∃ (Y) (∃ (X) (→ X Y Int))))
|
||||
(check-not-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
|
||||
as (∃ (Y) (∃ (X) (→ X Y Int))))
|
||||
: (∃ (X) (∃ (X) (→ X X Int))))
|
||||
|
||||
; cant typecheck bc X has local scope, and no X elimination form
|
||||
;(check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] x) : X)
|
||||
|
||||
(check-type 0 : Int)
|
||||
(check-type (+ 0 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1)
|
||||
(typecheck-fail (open [x <= (pack (Int 0) as (∃ (X) X)) with] (+ x 1))) ; can't use as Int
|
||||
|
||||
(check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y)))
|
||||
(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z)))
|
||||
: (∃ (X) X) ⇒ 0)
|
||||
(check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z)))
|
||||
: (∃ (X) X) ⇒ #t)
|
||||
|
||||
;; example where the two binding X's are conflated, see exist.rkt for explanation
|
||||
(check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] ((λ ([y : X]) 1) x))
|
||||
: Int ⇒ 1)
|
||||
|
||||
(check-type
|
||||
(pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [a : X] [f : (→ X X)])))
|
||||
: (∃ (X) (× [a : X] [f : (→ X X)])))
|
||||
|
||||
(define p4
|
||||
(pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [a : X] [f : (→ X Int)]))))
|
||||
(check-type p4 : (∃ (X) (× [a : X] [f : (→ X Int)])))
|
||||
|
||||
(check-not-type (open [x <= p4 with X] (proj x a)) : Int) ; type is X, not Int
|
||||
; type is (→ X X), not (→ Int Int)
|
||||
(check-not-type (open [x <= p4 with X] (proj x f)) : (→ Int Int))
|
||||
(typecheck-fail (open [x <= p4 with X] (+ 1 (proj x a))))
|
||||
(check-type (open [x <= p4 with X] ((proj x f) (proj x a))) : Int ⇒ 6)
|
||||
(check-type (open [x <= p4 with X] ((λ ([y : X]) ((proj x f) y)) (proj x a))) : Int ⇒ 6)
|
||||
|
||||
(check-type
|
||||
(open [x <= (pack (Int 0) as (∃ (Y) Y)) with X]
|
||||
((λ ([y : X]) 1) x))
|
||||
: Int ⇒ 1)
|
||||
|
||||
(check-type
|
||||
(pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [a : Int] [f : (→ Int Int)])))
|
||||
: (∃ (X) (× [a : Int] [f : (→ Int Int)])))
|
||||
|
||||
(typecheck-fail
|
||||
(pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [a : Int] [f : (→ Bool Int)]))))
|
||||
|
||||
(typecheck-fail
|
||||
(pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))]))
|
||||
as (∃ (X) (× [a : X] [f : (→ X Bool)]))))
|
||||
|
||||
(check-type
|
||||
(pack (Bool (tup [a = #t] [f = (λ ([x : Bool]) (if x 1 2))]))
|
||||
as (∃ (X) (× [a : X] [f : (→ X Int)])))
|
||||
: (∃ (X) (× [a : X] [f : (→ X Int)])))
|
||||
|
||||
(define counterADT
|
||||
(pack (Int (tup [new = 1]
|
||||
[get = (λ ([i : Int]) i)]
|
||||
[inc = (λ ([i : Int]) (+ i 1))]))
|
||||
as (∃ (Counter) (× [new : Counter]
|
||||
[get : (→ Counter Int)]
|
||||
[inc : (→ Counter Counter)]))))
|
||||
(check-type counterADT :
|
||||
(∃ (Counter) (× [new : Counter]
|
||||
[get : (→ Counter Int)]
|
||||
[inc : (→ Counter Counter)])))
|
||||
(typecheck-fail
|
||||
(open [counter <= counterADT with Counter]
|
||||
(+ (proj counter new) 1))
|
||||
#:with-msg "expected: +Int, Int\n *given: +Counter, Int\n *expressions: \\(proj counter new\\), 1")
|
||||
(typecheck-fail
|
||||
(open [counter <= counterADT with Counter]
|
||||
((λ ([x : Int]) x) (proj counter new)))
|
||||
#:with-msg "expected: +Int\n *given: +Counter\n *expressions: \\(proj counter new\\)")
|
||||
(check-type
|
||||
(open [counter <= counterADT with Counter]
|
||||
((proj counter get) ((proj counter inc) (proj counter new))))
|
||||
: Int ⇒ 2)
|
||||
|
||||
(check-type
|
||||
(open [counter <= counterADT with Counter]
|
||||
(let ([inc (proj counter inc)]
|
||||
[get (proj counter get)])
|
||||
(let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))])
|
||||
(get (add3 (proj counter new))))))
|
||||
: Int ⇒ 4)
|
||||
|
||||
(check-type
|
||||
(open [counter <= counterADT with Counter]
|
||||
(let ([get (proj counter get)]
|
||||
[inc (proj counter inc)]
|
||||
[new (λ () (proj counter new))])
|
||||
(letrec ([(is-even? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(or (zero? n)
|
||||
(is-odd? (sub1 n))))]
|
||||
[(is-odd? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(and (not (zero? n))
|
||||
(is-even? (sub1 n))))])
|
||||
(open [flipflop <=
|
||||
(pack (Counter (tup [new = (new)]
|
||||
[read = (λ ([c : Counter]) (is-even? (get c)))]
|
||||
[toggle = (λ ([c : Counter]) (inc c))]
|
||||
[reset = (λ ([c : Counter]) (new))]))
|
||||
as (∃ (FlipFlop) (× [new : FlipFlop]
|
||||
[read : (→ FlipFlop Bool)]
|
||||
[toggle : (→ FlipFlop FlipFlop)]
|
||||
[reset : (→ FlipFlop FlipFlop)])))
|
||||
with FlipFlop]
|
||||
(let ([read (proj flipflop read)]
|
||||
[togg (proj flipflop toggle)])
|
||||
(read (togg (togg (togg (togg (proj flipflop new)))))))))))
|
||||
: Bool ⇒ #f)
|
||||
|
||||
(define counterADT2
|
||||
(pack ((× [x : Int])
|
||||
(tup [new = (tup [x = 1])]
|
||||
[get = (λ ([i : (× [x : Int])]) (proj i x))]
|
||||
[inc = (λ ([i : (× [x : Int])]) (tup [x = (+ 1 (proj i x))]))]))
|
||||
as (∃ (Counter) (× [new : Counter]
|
||||
[get : (→ Counter Int)]
|
||||
[inc : (→ Counter Counter)]))))
|
||||
(check-type counterADT2 :
|
||||
(∃ (Counter) (× [new : Counter]
|
||||
[get : (→ Counter Int)]
|
||||
[inc : (→ Counter Counter)])))
|
||||
|
||||
;; same as above, but with different internal counter representation
|
||||
(check-type
|
||||
(open [counter <= counterADT2 with Counter]
|
||||
(let ([get (proj counter get)]
|
||||
[inc (proj counter inc)]
|
||||
[new (λ () (proj counter new))])
|
||||
(letrec ([(is-even? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(or (zero? n)
|
||||
(is-odd? (sub1 n))))]
|
||||
[(is-odd? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(and (not (zero? n))
|
||||
(is-even? (sub1 n))))])
|
||||
(open [flipflop <=
|
||||
(pack (Counter (tup [new = (new)]
|
||||
[read = (λ ([c : Counter]) (is-even? (get c)))]
|
||||
[toggle = (λ ([c : Counter]) (inc c))]
|
||||
[reset = (λ ([c : Counter]) (new))]))
|
||||
as (∃ (FlipFlop) (× [new : FlipFlop]
|
||||
[read : (→ FlipFlop Bool)]
|
||||
[toggle : (→ FlipFlop FlipFlop)]
|
||||
[reset : (→ FlipFlop FlipFlop)])))
|
||||
with
|
||||
FlipFlop]
|
||||
(let ([read (proj flipflop read)]
|
||||
[togg (proj flipflop toggle)])
|
||||
(read (togg (togg (togg (togg (proj flipflop new)))))))))))
|
||||
: Bool ⇒ #f)
|
||||
|
||||
;; err cases
|
||||
(typecheck-fail
|
||||
(pack (Int 1) as Int)
|
||||
#:with-msg
|
||||
"Expected ∃ type, got: Int")
|
||||
(typecheck-fail
|
||||
(open [x <= 2 with X] 3)
|
||||
#:with-msg
|
||||
"Expected ∃ type, got: Int")
|
||||
|
||||
;; previous tets from stlc+reco+var-tests.rkt ---------------------------------
|
||||
;; define-type-alias
|
||||
(define-type-alias Integer Int)
|
||||
(define-type-alias ArithBinOp (→ Int Int Int))
|
||||
;(define-type-alias C Complex) ; error, Complex undefined
|
||||
|
||||
(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
|
||||
(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)
|
||||
(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer)
|
||||
(check-type + : ArithBinOp)
|
||||
(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
|
||||
|
||||
;; records (ie labeled tuples)
|
||||
(check-type "Stephen" : String)
|
||||
(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [name : String] [phone : Int] [male? : Bool]))
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
|
||||
: String ⇒ "Stephen")
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
|
||||
: String ⇒ "Stephen")
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
|
||||
: Int ⇒ 781)
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
|
||||
: Bool ⇒ #t)
|
||||
(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [my-name : String] [phone : Int] [male? : Bool]))
|
||||
(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [name : String] [my-phone : Int] [male? : Bool]))
|
||||
(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [name : String] [phone : Int] [is-male? : Bool]))
|
||||
|
||||
;; variants
|
||||
(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
|
||||
(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
|
||||
(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
|
||||
(var coffee = (void) as (∨ [coffee : Unit]))))
|
||||
(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
|
||||
(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
|
||||
: (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
|
||||
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1])) ; not enough clauses
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1]
|
||||
[teaaaaaa x => 2])) ; wrong clause
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1]
|
||||
[tea x => 2]
|
||||
[coke x => 3])) ; too many clauses
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => "1"]
|
||||
[tea x => 2])) ; mismatched branch types
|
||||
(check-type
|
||||
(case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
|
||||
[coffee x => x]
|
||||
[tea x => 2]) : Int ⇒ 1)
|
||||
(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
|
||||
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
|
||||
(check-type
|
||||
(case ((λ ([d : Drink]) d)
|
||||
(var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
|
||||
[coffee x => (+ (+ x x) (+ x x))]
|
||||
[tea x => 2]
|
||||
[coke y => 3])
|
||||
: Int ⇒ 4)
|
||||
|
||||
(check-type
|
||||
(case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
|
||||
[coffee x => (+ (+ x x) (+ x x))]
|
||||
[tea x => 2]
|
||||
[coke y => 3])
|
||||
: Int ⇒ 4)
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
;; tests for tuples -----------------------------------------------------------
|
||||
;; old tuple syntax not supported here
|
||||
;(check-type (tup 1 2 3) : (× Int Int Int))
|
||||
;(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
|
||||
;(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
|
||||
;(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
|
||||
;(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
|
||||
;(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
|
||||
;
|
||||
;(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
|
||||
;(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
|
||||
;(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
|
||||
;(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
|
||||
;(typecheck-fail (proj 1 2)) ; not tuple
|
||||
|
||||
;; ext-stlc.rkt tests ---------------------------------------------------------
|
||||
;; should still pass
|
||||
|
||||
;; new literals and base types
|
||||
(check-type "one" : String) ; literal now supported
|
||||
(check-type #f : Bool) ; literal now supported
|
||||
|
||||
(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
|
||||
|
||||
;; Unit
|
||||
(check-type (void) : Unit)
|
||||
(check-type void : (→ Unit))
|
||||
(typecheck-fail ((λ ([x : Unit]) x) 2))
|
||||
(typecheck-fail ((λ ([x : Unit])) void))
|
||||
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
|
||||
|
||||
;; begin
|
||||
(typecheck-fail (begin))
|
||||
(check-type (begin 1) : Int)
|
||||
;(typecheck-fail (begin 1 2 3))
|
||||
(check-type (begin (void) 1) : Int ⇒ 1)
|
||||
|
||||
;;ascription
|
||||
(typecheck-fail (ann 1 : Bool))
|
||||
(check-type (ann 1 : Int) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
|
||||
|
||||
; let
|
||||
(check-type (let () (+ 1 1)) : Int ⇒ 2)
|
||||
(check-type (let ([x 10]) (+ 1 2)) : Int)
|
||||
(typecheck-fail (let ([x #f]) (+ x 1)))
|
||||
(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
|
||||
(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
|
||||
|
||||
(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
|
||||
(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
|
||||
|
||||
; letrec
|
||||
(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
|
||||
(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
|
||||
|
||||
(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
|
||||
|
||||
;; recursive
|
||||
(check-type
|
||||
(letrec ([(countdown : (→ Int String))
|
||||
(λ ([i : Int])
|
||||
(if (= i 0)
|
||||
"liftoff"
|
||||
(countdown (- i 1))))])
|
||||
(countdown 10)) : String ⇒ "liftoff")
|
||||
|
||||
;; mutually recursive
|
||||
(check-type
|
||||
(letrec ([(is-even? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(or (zero? n)
|
||||
(is-odd? (sub1 n))))]
|
||||
[(is-odd? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(and (not (zero? n))
|
||||
(is-even? (sub1 n))))])
|
||||
(is-odd? 11)) : Bool ⇒ #t)
|
||||
|
||||
;; tests from stlc+lit-tests.rkt --------------------------
|
||||
; most should pass, some failing may now pass due to added types/forms
|
||||
(check-type 1 : Int)
|
||||
;(check-not-type 1 : (Int → Int))
|
||||
;(typecheck-fail "one") ; literal now supported
|
||||
;(typecheck-fail #f) ; literal now supported
|
||||
(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 now valid type, but arg has wrong type
|
||||
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now 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)
|
||||
|
||||
211
macrotypes/examples/tests/fomega-tests.rkt
Normal file
211
macrotypes/examples/tests/fomega-tests.rkt
Normal file
|
|
@ -0,0 +1,211 @@
|
|||
#lang s-exp "../fomega.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(check-type Int : ★)
|
||||
(check-type String : ★)
|
||||
(typecheck-fail →)
|
||||
(check-type (→ Int Int) : ★)
|
||||
(typecheck-fail (→ →))
|
||||
(typecheck-fail (→ 1))
|
||||
(check-type 1 : Int)
|
||||
|
||||
(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid type: 1")
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
|
||||
(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
|
||||
(∀ ([X : (∀★ ★)]) (→ X X)))
|
||||
|
||||
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
|
||||
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
|
||||
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
|
||||
|
||||
(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
|
||||
: (∀ ([X : ★]) (→ X X)))
|
||||
(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (⇒ ★ ★)]) (λ ([x : X]) x))))
|
||||
|
||||
(check-type (tyλ ([t : ★]) t) : (⇒ ★ ★))
|
||||
(check-type (tyλ ([t : ★] [s : ★]) t) : (⇒ ★ ★ ★))
|
||||
(check-type (tyλ ([t : ★]) (tyλ ([s : ★]) t)) : (⇒ ★ (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t : (⇒ ★ ★)]) t) : (⇒ (⇒ ★ ★) (⇒ ★ ★)))
|
||||
(check-type (tyλ ([t : (⇒ ★ ★ ★)]) t) : (⇒ (⇒ ★ ★ ★) (⇒ ★ ★ ★)))
|
||||
(check-type (tyλ ([arg : ★] [res : ★]) (→ arg res)) : (⇒ ★ ★ ★))
|
||||
|
||||
(check-type (tyapp (tyλ ([t : ★]) t) Int) : ★)
|
||||
(check-type (λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) : (→ Int Int))
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
|
||||
(check-type ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
|
||||
(typecheck-fail ((λ ([x : (tyapp (tyλ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
|
||||
|
||||
;; partial-apply →
|
||||
(check-type (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)
|
||||
: (⇒ ★ ★))
|
||||
;; f's type must have kind ★
|
||||
(typecheck-fail (λ ([f : (tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int)]) f))
|
||||
(check-type (Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f)) :
|
||||
(∀ ([tyf : (⇒ ★ ★)]) (→ (tyapp tyf String) (tyapp tyf String))))
|
||||
(check-type (inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
: (→ (→ Int String) (→ Int String)))
|
||||
(typecheck-fail
|
||||
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
|
||||
#:with-msg "inst: type mismatch\n *expected: +★\n *given: +Int\n *expressions: 1")
|
||||
|
||||
(typecheck-fail
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
#:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
|
||||
;; applied f too early
|
||||
(typecheck-fail
|
||||
(inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
#:with-msg "Expected → type, got: \\(tyapp tyf String\\)")
|
||||
(check-type ((inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) : (→ Int String))
|
||||
(check-type (((inst
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) f))
|
||||
(tyapp (tyλ ([arg : ★]) (tyλ ([res : ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) 1) : String ⇒ "int")
|
||||
|
||||
;; tapl examples, p441
|
||||
(typecheck-fail
|
||||
(define-type-alias tmp 1)
|
||||
#:with-msg "not a valid type: 1")
|
||||
(define-type-alias Id (tyλ ([X : ★]) X))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (tyapp Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int (tyapp Id String))]) 1) : (→ (→ Int (tyapp Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) (tyapp Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (tyapp Id Int) String) Int))
|
||||
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (tyapp Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (tyapp Id (→ Int String))]) 1) : (→ (tyapp Id (tyapp Id (→ Int String))) Int))
|
||||
|
||||
;; tapl examples, p451
|
||||
(define-type-alias Pair (tyλ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
|
||||
|
||||
;(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")
|
||||
|
||||
;; 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 (Λ ([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-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))
|
||||
|
||||
;; 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)
|
||||
203
macrotypes/examples/tests/fomega2-tests.rkt
Normal file
203
macrotypes/examples/tests/fomega2-tests.rkt
Normal file
|
|
@ -0,0 +1,203 @@
|
|||
#lang s-exp "../fomega2.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(check-type Int : ★)
|
||||
(check-type String : ★)
|
||||
(typecheck-fail →)
|
||||
(check-type (→ Int Int) : ★)
|
||||
(typecheck-fail (→ →))
|
||||
(typecheck-fail (→ 1))
|
||||
(check-type 1 : Int)
|
||||
|
||||
;; this should error but it doesnt
|
||||
#;(λ ([x : ★]) 1)
|
||||
|
||||
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
|
||||
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
|
||||
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
|
||||
|
||||
(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
|
||||
: (∀ ([X : ★]) (→ X X)))
|
||||
(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
|
||||
|
||||
(check-type (λ ([t : ★]) t) : (→ ★ ★))
|
||||
(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
|
||||
(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
|
||||
(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
|
||||
(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
|
||||
(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
|
||||
|
||||
(check-type ((λ ([t : ★]) t) Int) : ★)
|
||||
(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
|
||||
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
|
||||
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
|
||||
(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
|
||||
|
||||
;; partial-apply →
|
||||
(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
|
||||
: (→ ★ ★))
|
||||
; f's type must have kind ★
|
||||
(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
|
||||
(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
|
||||
(∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
|
||||
(check-type (inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
|
||||
: (→ (→ Int String) (→ Int String)))
|
||||
(typecheck-fail
|
||||
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
|
||||
;#:with-msg "not a valid type: 1")
|
||||
|
||||
;; applied f too early
|
||||
(typecheck-fail (inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
|
||||
(check-type ((inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) : (→ Int String))
|
||||
(check-type (((inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) 1) : String ⇒ "int")
|
||||
|
||||
;; tapl examples, p441
|
||||
(typecheck-fail
|
||||
(define-type-alias tmp 1))
|
||||
;#:with-msg "not a valid type: 1")
|
||||
(define-type-alias Id (λ ([X : ★]) X))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
|
||||
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
|
||||
|
||||
;; tapl examples, p451
|
||||
(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
|
||||
|
||||
;(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 (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 (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")
|
||||
: (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 : ★]) (→ (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)
|
||||
: (→ (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 : ★]) (→ (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)
|
||||
: (→ (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)))
|
||||
|
||||
(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))))
|
||||
: (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ 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))
|
||||
|
||||
;; 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)
|
||||
200
macrotypes/examples/tests/fomega3-tests.rkt
Normal file
200
macrotypes/examples/tests/fomega3-tests.rkt
Normal file
|
|
@ -0,0 +1,200 @@
|
|||
#lang s-exp "../fomega3.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(check-type Int : ★)
|
||||
(check-type String : ★)
|
||||
(typecheck-fail →)
|
||||
(check-type (→ Int Int) : ★)
|
||||
(typecheck-fail (→ →))
|
||||
(typecheck-fail (→ 1))
|
||||
(check-type 1 : Int)
|
||||
|
||||
;(check-type (∀ ([t : ★]) (→ t t)) : ★)
|
||||
(check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
|
||||
(check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
|
||||
|
||||
(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
|
||||
|
||||
(check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x)))
|
||||
: (∀ ([X : ★]) (→ X X)))
|
||||
(typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x))))
|
||||
|
||||
(check-type (λ ([t : ★]) t) : (→ ★ ★))
|
||||
(check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★))
|
||||
(check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★)))
|
||||
(check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★)))
|
||||
(check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★)))
|
||||
(check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★))
|
||||
|
||||
(check-type ((λ ([t : ★]) t) Int) : ★)
|
||||
(check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int))
|
||||
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2)
|
||||
(check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2)
|
||||
(typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string"))
|
||||
|
||||
;; partial-apply →
|
||||
(check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)
|
||||
: (→ ★ ★))
|
||||
; f's type must have kind ★
|
||||
(typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f))
|
||||
(check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) :
|
||||
(∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String))))
|
||||
(check-type (inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
|
||||
: (→ (→ Int String) (→ Int String)))
|
||||
(typecheck-fail
|
||||
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1))
|
||||
;#:with-msg "not a valid type: 1")
|
||||
|
||||
;; applied f too early
|
||||
(typecheck-fail (inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1)))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)))
|
||||
(check-type ((inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) : (→ Int String))
|
||||
(check-type (((inst
|
||||
(Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f))
|
||||
((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))
|
||||
(λ ([x : Int]) "int")) 1) : String ⇒ "int")
|
||||
|
||||
;; tapl examples, p441
|
||||
(typecheck-fail
|
||||
(define-type-alias tmp 1))
|
||||
;#:with-msg "not a valid type: 1")
|
||||
(define-type-alias Id (λ ([X : ★]) X))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int))
|
||||
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int))
|
||||
(check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int))
|
||||
(check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int))
|
||||
|
||||
;; tapl examples, p451
|
||||
(define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X))))
|
||||
|
||||
;(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 (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 (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")
|
||||
: (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 : ★]) (→ (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)
|
||||
: (→ (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 : ★]) (→ (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)
|
||||
: (→ (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)))
|
||||
|
||||
(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))))
|
||||
: (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ 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))
|
||||
|
||||
;; 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)
|
||||
153
macrotypes/examples/tests/fsub-tests.rkt
Normal file
153
macrotypes/examples/tests/fsub-tests.rkt
Normal file
|
|
@ -0,0 +1,153 @@
|
|||
#lang s-exp "../fsub.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; examples from tapl ch26, bounded quantification
|
||||
;; (same tests from stlc+reco+sub.rkt, but last one should not typecheck)
|
||||
(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
|
||||
|
||||
(define ra (tup [a = 0]))
|
||||
(check-type ((λ ([x : (× [a : Int])]) x) ra)
|
||||
: (× [a : Int]) ⇒ (tup [a = 0]))
|
||||
(define rab (tup [a = 0][b = #t]))
|
||||
(check-type ((λ ([x : (× [a : Int])]) x) rab)
|
||||
: (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
|
||||
|
||||
(check-type (proj ((λ ([x : (× [a : Int])]) x) rab) a)
|
||||
: Int ⇒ 0)
|
||||
|
||||
(check-type (Λ ([X <: Top]) (λ ([x : X]) x)) : (∀ ([X <: Top]) (→ X X)))
|
||||
(check-type (inst (Λ ([X <: Top]) (λ ([x : X]) x)) (× [a : Int][b : Bool]))
|
||||
: (→ (× [a : Int][b : Bool]) (× [a : Int][b : Bool])))
|
||||
|
||||
(check-type (proj ((inst (Λ ([X <: Top]) (λ ([x : X]) x))
|
||||
(× [a : Int][b : Bool]))
|
||||
rab) b)
|
||||
: Bool ⇒ #t)
|
||||
|
||||
(define f2 (λ ([x : (× [a : Nat])]) (tup [orig = x] [asucc = (+ 1 (proj x a))])))
|
||||
(check-type f2 : (→ (× [a : Nat]) (× [orig : (× [a : Nat])] [asucc : Nat])))
|
||||
(check-type (f2 ra) : (× [orig : (× [a : Nat])][asucc : Nat]))
|
||||
(check-type (f2 rab) : (× [orig : (× [a : Nat])][asucc : Nat]))
|
||||
|
||||
; check expose properly called for primops
|
||||
(define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1))))
|
||||
(check-type fNat : (∀ ([X <: Nat]) (→ X Nat)))
|
||||
|
||||
;; check type constructors properly call expose
|
||||
(define f2poly
|
||||
(Λ ([X <: (× [a : Nat])])
|
||||
(λ ([x : X])
|
||||
(tup [orig = x][asucc = (+ (proj x a) 1)]))))
|
||||
|
||||
(check-type f2poly : (∀ ([X <: (× [a : Nat])]) (→ X (× [orig : X][asucc : Nat]))))
|
||||
|
||||
; inst f2poly with (× [a : Nat])
|
||||
(check-type (inst f2poly (× [a : Nat]))
|
||||
: (→ (× [a : Nat])
|
||||
(× [orig : (× [a : Nat])][asucc : Nat])))
|
||||
(check-type ((inst f2poly (× [a : Nat])) ra)
|
||||
: (× [orig : (× [a : Nat])][asucc : Nat])
|
||||
⇒ (tup [orig = ra][asucc = 1]))
|
||||
|
||||
(check-type ((inst f2poly (× [a : Nat])) rab)
|
||||
: (× [orig : (× [a : Nat])][asucc : Nat])
|
||||
⇒ (tup [orig = rab][asucc = 1]))
|
||||
|
||||
(typecheck-fail (proj (proj ((inst f2poly (× [a : Nat])) rab) orig) b))
|
||||
|
||||
;; inst f2poly with (× [a : Nat][b : Bool])
|
||||
(check-type (inst f2poly (× [a : Nat][b : Bool]))
|
||||
: (→ (× [a : Nat][b : Bool])
|
||||
(× [orig : (× [a : Nat][b : Bool])][asucc : Nat])))
|
||||
(typecheck-fail ((inst f2poly (× [a : Nat][b : Bool])) ra))
|
||||
|
||||
(check-type ((inst f2poly (× [a : Nat][b : Bool])) rab)
|
||||
: (× [orig : (× [a : Nat][b : Bool])][asucc : Nat])
|
||||
⇒ (tup [orig = rab][asucc = 1]))
|
||||
|
||||
(check-type (proj (proj ((inst f2poly (× [a : Nat][b : Bool])) rab) orig) b)
|
||||
: Bool ⇒ #t)
|
||||
|
||||
;; make sure inst still checks args
|
||||
(typecheck-fail (inst (Λ ([X <: Nat]) 1) Int))
|
||||
|
||||
; ch28
|
||||
(define f (Λ ([X <: (→ Nat Nat)]) (λ ([y : X]) (y 5))))
|
||||
(check-type f : (∀ ([X <: (→ Nat Nat)]) (→ X Nat)))
|
||||
(check-type (inst f (→ Nat Nat)) : (→ (→ Nat Nat) Nat))
|
||||
(check-type (inst f (→ Int Nat)) : (→ (→ Int Nat) Nat))
|
||||
(typecheck-fail (inst f (→ Nat Int)))
|
||||
(check-type ((inst f (→ Int Nat)) (λ ([z : Int]) 5)) : Nat)
|
||||
(check-type ((inst f (→ Int Nat)) (λ ([z : Num]) 5)) : Nat)
|
||||
(typecheck-fail ((inst f (→ Int Nat)) (λ ([z : Nat]) 5)))
|
||||
|
||||
|
||||
;; old sysf tests -------------------------------------------------------------
|
||||
;; old syntax no longer valid
|
||||
;(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 (Λ (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-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))
|
||||
;
|
||||
;;;; 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))
|
||||
;; strings and boolean literals now ok
|
||||
;(typecheck-fail "one") ; unsupported literal
|
||||
;(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))
|
||||
;; edited from sysf test to handle subtyping
|
||||
(check-type ((λ ([f : (→ Nat Nat Nat)] [x : Nat] [y : Nat]) (f x y)) + 1 2) : Num ⇒ 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 : Nat]) (+ x x)) 10) : Num ⇒ 20)
|
||||
37
macrotypes/examples/tests/run-all-tests.rkt
Normal file
37
macrotypes/examples/tests/run-all-tests.rkt
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
#lang racket
|
||||
|
||||
;; stlc and extensions
|
||||
(require "stlc-tests.rkt")
|
||||
(require "stlc+lit-tests.rkt")
|
||||
(require "ext-stlc-tests.rkt")
|
||||
(require "stlc+tup-tests.rkt")
|
||||
(require "stlc+reco+var-tests.rkt")
|
||||
(require "stlc+cons-tests.rkt")
|
||||
(require "stlc+box-tests.rkt")
|
||||
|
||||
(require "stlc+rec-iso-tests.rkt")
|
||||
|
||||
(require "exist-tests.rkt")
|
||||
|
||||
;; subtyping
|
||||
(require "stlc+sub-tests.rkt")
|
||||
(require "stlc+reco+sub-tests.rkt")
|
||||
|
||||
;; system F
|
||||
(require "sysf-tests.rkt")
|
||||
|
||||
(require "fsub-tests.rkt") ; sysf + reco-sub
|
||||
|
||||
;; F_omega
|
||||
(require "fomega-tests.rkt")
|
||||
(require "fomega2-tests.rkt")
|
||||
(require "fomega3-tests.rkt")
|
||||
|
||||
(require "stlc+occurrence-tests.rkt")
|
||||
(require "stlc+overloading-tests.rkt")
|
||||
|
||||
;; type inference
|
||||
(require "infer-tests.rkt")
|
||||
|
||||
;; type and effects
|
||||
(require "stlc+effect-tests.rkt")
|
||||
247
macrotypes/examples/tests/stlc+rec-iso-tests.rkt
Normal file
247
macrotypes/examples/tests/stlc+rec-iso-tests.rkt
Normal file
|
|
@ -0,0 +1,247 @@
|
|||
#lang s-exp "../stlc+rec-iso.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(define-type-alias IntList (μ (X) (∨ [nil : Unit] [cons : (× Int X)])))
|
||||
(define-type-alias ILBody (∨ [nil : Unit] [cons : (× Int IntList)]))
|
||||
|
||||
;; nil
|
||||
(define nil (fld {IntList} (var nil = (void) as ILBody)))
|
||||
(check-type nil : IntList)
|
||||
|
||||
;; cons
|
||||
(define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var cons = (tup n lst) as ILBody))))
|
||||
(check-type cons : (→ Int IntList IntList))
|
||||
(check-type (cons 1 nil) : IntList)
|
||||
(typecheck-fail (cons 1 2))
|
||||
(typecheck-fail (cons "1" nil))
|
||||
|
||||
;; isnil
|
||||
(define isnil
|
||||
(λ ([lst : IntList])
|
||||
(case (unfld {IntList} lst)
|
||||
[nil n => #t]
|
||||
[cons p => #f])))
|
||||
(check-type isnil : (→ IntList Bool))
|
||||
(check-type (isnil nil) : Bool ⇒ #t)
|
||||
(check-type (isnil (cons 1 nil)) : Bool ⇒ #f)
|
||||
(typecheck-fail (isnil 1))
|
||||
(typecheck-fail (isnil (cons 1 2)))
|
||||
(check-type (λ ([f : (→ IntList Bool)]) (f nil)) : (→ (→ IntList Bool) Bool))
|
||||
(check-type ((λ ([f : (→ IntList Bool)]) (f nil)) isnil) : Bool ⇒ #t)
|
||||
|
||||
;; hd
|
||||
(define hd
|
||||
(λ ([lst : IntList])
|
||||
(case (unfld {IntList} lst)
|
||||
[nil n => 0]
|
||||
[cons p => (proj p 0)])))
|
||||
(check-type hd : (→ IntList Int))
|
||||
(check-type (hd nil) : Int ⇒ 0)
|
||||
(typecheck-fail (hd 1))
|
||||
(check-type (hd (cons 11 nil)) : Int ⇒ 11)
|
||||
|
||||
;; tl
|
||||
(define tl
|
||||
(λ ([lst : IntList])
|
||||
(case (unfld {IntList} lst)
|
||||
[nil n => lst]
|
||||
[cons p => (proj p 1)])))
|
||||
(check-type tl : (→ IntList IntList))
|
||||
(check-type (tl nil) : IntList ⇒ nil)
|
||||
(check-type (tl (cons 1 nil)) : IntList ⇒ nil)
|
||||
(check-type (tl (cons 1 (cons 2 nil))) : IntList ⇒ (cons 2 nil))
|
||||
(typecheck-fail (tl 1))
|
||||
|
||||
;; some typecheck failure msgs
|
||||
(typecheck-fail
|
||||
(fld {Int} 1)
|
||||
#:with-msg
|
||||
"Expected μ type, got: Int")
|
||||
(typecheck-fail
|
||||
(unfld {Int} 1)
|
||||
#:with-msg
|
||||
"Expected μ type, got: Int")
|
||||
|
||||
;; previous stlc+var tests ----------------------------------------------------
|
||||
;; define-type-alias
|
||||
(define-type-alias Integer Int)
|
||||
(define-type-alias ArithBinOp (→ Int Int Int))
|
||||
;(define-type-alias C Complex) ; error, Complex undefined
|
||||
|
||||
(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
|
||||
(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)
|
||||
(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer)
|
||||
(check-type + : ArithBinOp)
|
||||
(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
|
||||
|
||||
;; records (ie labeled tuples)
|
||||
; no records, only tuples
|
||||
(check-type "Stephen" : String)
|
||||
;(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
|
||||
; (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
|
||||
;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
|
||||
; : String ⇒ "Stephen")
|
||||
;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
|
||||
; : String ⇒ "Stephen")
|
||||
;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
|
||||
; : Int ⇒ 781)
|
||||
;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
|
||||
; : Bool ⇒ #t)
|
||||
;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
|
||||
; (× [: "my-name" String] [: "phone" Int] [: "male?" Bool]))
|
||||
;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
|
||||
; (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
|
||||
;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
|
||||
; (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
|
||||
|
||||
;; variants
|
||||
(check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit]))
|
||||
(check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
|
||||
(typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x)
|
||||
(var coffee = (void) as (∨ [coffee : Unit]))))
|
||||
(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit]))
|
||||
(check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
|
||||
: (∨ [coffee : Unit] [tea : Unit] [coke : Unit]))
|
||||
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1])) ; not enough clauses
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1]
|
||||
[teaaaaaa x => 2])) ; wrong clause
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => 1]
|
||||
[tea x => 2]
|
||||
[coke x => 3])) ; too many clauses
|
||||
(typecheck-fail
|
||||
(case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit]))
|
||||
[coffee x => "1"]
|
||||
[tea x => 2])) ; mismatched branch types
|
||||
(check-type
|
||||
(case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit]))
|
||||
[coffee x => x]
|
||||
[tea x => 2]) : Int ⇒ 1)
|
||||
(define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool]))
|
||||
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
|
||||
(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
|
||||
(check-type
|
||||
(case ((λ ([d : Drink]) d)
|
||||
(var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool])))
|
||||
[coffee x => (+ (+ x x) (+ x x))]
|
||||
[tea x => 2]
|
||||
[coke y => 3])
|
||||
: Int ⇒ 4)
|
||||
|
||||
(check-type
|
||||
(case ((λ ([d : Drink]) d) (var coffee = 1 as Drink))
|
||||
[coffee x => (+ (+ x x) (+ x x))]
|
||||
[tea x => 2]
|
||||
[coke y => 3])
|
||||
: Int ⇒ 4)
|
||||
|
||||
;; previous tests: ------------------------------------------------------------
|
||||
;; tests for tuples -----------------------------------------------------------
|
||||
(check-type (tup 1 2 3) : (× Int Int Int))
|
||||
(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
|
||||
(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
|
||||
(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
|
||||
(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
|
||||
(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
|
||||
|
||||
(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
|
||||
(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
|
||||
(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
|
||||
(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
|
||||
(typecheck-fail
|
||||
(proj 1 2)
|
||||
#:with-msg
|
||||
"Expected × type, got: Int")
|
||||
|
||||
;; ext-stlc.rkt tests ---------------------------------------------------------
|
||||
;; should still pass
|
||||
|
||||
;; new literals and base types
|
||||
(check-type "one" : String) ; literal now supported
|
||||
(check-type #f : Bool) ; literal now supported
|
||||
|
||||
(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
|
||||
|
||||
;; Unit
|
||||
(check-type (void) : Unit)
|
||||
(check-type void : (→ Unit))
|
||||
(typecheck-fail ((λ ([x : Unit]) x) 2))
|
||||
(typecheck-fail ((λ ([x : Unit])) void))
|
||||
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
|
||||
|
||||
;; begin
|
||||
(typecheck-fail (begin))
|
||||
(check-type (begin 1) : Int)
|
||||
;(typecheck-fail (begin 1 2 3))
|
||||
(check-type (begin (void) 1) : Int ⇒ 1)
|
||||
|
||||
;;ascription
|
||||
(typecheck-fail (ann 1 : Bool))
|
||||
(check-type (ann 1 : Int) : Int ⇒ 1)
|
||||
(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
|
||||
|
||||
; let
|
||||
(check-type (let () (+ 1 1)) : Int ⇒ 2)
|
||||
(check-type (let ([x 10]) (+ 1 2)) : Int)
|
||||
(typecheck-fail (let ([x #f]) (+ x 1)))
|
||||
(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
|
||||
(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
|
||||
|
||||
(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
|
||||
(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
|
||||
|
||||
; letrec
|
||||
(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
|
||||
(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
|
||||
|
||||
(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
|
||||
|
||||
;; recursive
|
||||
(check-type
|
||||
(letrec ([(countdown : (→ Int String))
|
||||
(λ ([i : Int])
|
||||
(if (= i 0)
|
||||
"liftoff"
|
||||
(countdown (- i 1))))])
|
||||
(countdown 10)) : String ⇒ "liftoff")
|
||||
|
||||
;; mutually recursive
|
||||
(check-type
|
||||
(letrec ([(is-even? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(or (zero? n)
|
||||
(is-odd? (sub1 n))))]
|
||||
[(is-odd? : (→ Int Bool))
|
||||
(λ ([n : Int])
|
||||
(and (not (zero? n))
|
||||
(is-even? (sub1 n))))])
|
||||
(is-odd? 11)) : Bool ⇒ #t)
|
||||
|
||||
;; tests from stlc+lit-tests.rkt --------------------------
|
||||
; most should pass, some failing may now pass due to added types/forms
|
||||
(check-type 1 : Int)
|
||||
;(check-not-type 1 : (Int → Int))
|
||||
;(typecheck-fail "one") ; literal now supported
|
||||
;(typecheck-fail #f) ; literal now supported
|
||||
(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 now valid type, but arg has wrong type
|
||||
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now 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)
|
||||
|
||||
113
macrotypes/examples/tests/stlc+reco+sub-tests.rkt
Normal file
113
macrotypes/examples/tests/stlc+reco+sub-tests.rkt
Normal file
|
|
@ -0,0 +1,113 @@
|
|||
#lang s-exp "../stlc+reco+sub.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; record subtyping tests
|
||||
(check-type "coffee" : String)
|
||||
(check-type (tup [coffee = 3]) : (× [coffee : Int])) ; element subtyping
|
||||
(check-type (var coffee = 3 as (∨ [coffee : Nat])) : (∨ [coffee : Int])) ; element subtyping
|
||||
;err
|
||||
(typecheck-fail
|
||||
(var cooffee = 3 as (∨ [coffee : Nat]))
|
||||
#:with-msg "cooffee field does not exist")
|
||||
(check-type (tup [coffee = 3]) : (× [coffee : Nat]))
|
||||
(check-type (tup [coffee = 3]) : (× [coffee : Top]))
|
||||
(check-type (var coffee = 3 as (∨ [coffee : Int])) : (∨ [coffee : Top])) ; element subtyping (twice)
|
||||
(check-type (tup [coffee = 3]) : (× [coffee : Num]))
|
||||
(check-not-type (tup [coffee = -3]) : (× [coffee : Nat]))
|
||||
(check-type (tup [coffee = -3]) : (× [coffee : Num]))
|
||||
(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Int])) ; width subtyping
|
||||
(check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Num])) ; width+element subtyping
|
||||
|
||||
;; record + fns
|
||||
(check-type (tup [plus = +]) : (× [plus : (→ Num Num Num)]))
|
||||
(check-type + : (→ Num Num Num))
|
||||
(check-type (tup [plus = +]) : (× [plus : (→ Int Num Num)]))
|
||||
(check-type (tup [plus = +]) : (× [plus : (→ Int Num Top)]))
|
||||
(check-type (tup [plus = +] [mul = *]) : (× [plus : (→ Int Num Top)]))
|
||||
|
||||
;; examples from tapl ch26, bounded quantification
|
||||
(check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int])))
|
||||
|
||||
(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0]))
|
||||
: (× [a : Int]) ⇒ (tup [a = 0]))
|
||||
(check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t]))
|
||||
: (× [a : Int]) ⇒ (tup [a = 0][b = #t]))
|
||||
|
||||
(check-type (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) a)
|
||||
: Int ⇒ 0)
|
||||
|
||||
;; this should work! but needs bounded quantification, see fsub.rkt
|
||||
(typecheck-fail (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) b))
|
||||
|
||||
; conditional
|
||||
(check-not-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Nat))
|
||||
(check-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Int))
|
||||
(check-not-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Nat))
|
||||
(check-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Int))
|
||||
(check-type (λ ([x : Bool]) (if x "1" 1)) : (→ Bool Top))
|
||||
|
||||
;; previous record tests ------------------------------------------------------
|
||||
;; records (ie labeled tuples)
|
||||
(check-type "Stephen" : String)
|
||||
(check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [name : String] [phone : Int] [male? : Bool]))
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
|
||||
: String ⇒ "Stephen")
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name)
|
||||
: String ⇒ "Stephen")
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone)
|
||||
: Int ⇒ 781)
|
||||
(check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?)
|
||||
: Bool ⇒ #t)
|
||||
(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [my-name : String] [phone : Int] [male? : Bool]))
|
||||
(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [name : String] [my-phone : Int] [male? : Bool]))
|
||||
(check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) :
|
||||
(× [name : String] [phone : Int] [is-male? : Bool]))
|
||||
|
||||
|
||||
;; previous basic subtyping tests ------------------------------------------------------
|
||||
(check-type 1 : Top)
|
||||
(check-type 1 : Num)
|
||||
(check-type 1 : Int)
|
||||
(check-type 1 : Nat)
|
||||
(check-type -1 : Top)
|
||||
(check-type -1 : Num)
|
||||
(check-type -1 : Int)
|
||||
(check-not-type -1 : Nat)
|
||||
(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1)
|
||||
(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1)
|
||||
(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
|
||||
(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
|
||||
(typecheck-fail ((λ ([x : Nat]) x) -1))
|
||||
(check-type (λ ([x : Int]) x) : (→ Int Int))
|
||||
(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
|
||||
(check-not-type (λ ([x : Int]) x) : (→ Int Nat))
|
||||
(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
|
||||
(check-not-type (λ ([x : Int]) x) : (→ Num Int))
|
||||
|
||||
;; previous tests -------------------------------------------------------------
|
||||
;; some change due to more specific types
|
||||
(check-type 1 : Int)
|
||||
(check-not-type 1 : (→ Int Int))
|
||||
;(typecheck-fail "one") ; unsupported literal
|
||||
;(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)
|
||||
; Bool now defined
|
||||
;(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)
|
||||
;; changed test
|
||||
(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20)
|
||||
63
macrotypes/examples/tests/stlc+sub-tests.rkt
Normal file
63
macrotypes/examples/tests/stlc+sub-tests.rkt
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
#lang s-exp "../stlc+sub.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
;; subtyping tests
|
||||
(check-type 1 : Top)
|
||||
(check-type 1 : Num)
|
||||
(check-type 1 : Int)
|
||||
(check-type 1 : Nat)
|
||||
(check-type -1 : Top)
|
||||
(check-type -1 : Num)
|
||||
(check-type -1 : Int)
|
||||
(check-not-type -1 : Nat)
|
||||
(check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1)
|
||||
(check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1)
|
||||
(check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
|
||||
(check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
|
||||
(typecheck-fail ((λ ([x : Nat]) x) -1))
|
||||
(check-type (λ ([x : Int]) x) : (→ Int Int))
|
||||
(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
|
||||
(check-not-type (λ ([x : Int]) x) : (→ Int Nat))
|
||||
(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
|
||||
(check-not-type (λ ([x : Int]) x) : (→ Num Int))
|
||||
|
||||
(check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0)
|
||||
(check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2)
|
||||
(typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1))
|
||||
(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2)
|
||||
(typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1))
|
||||
|
||||
(check-type + : (→ Num Num Num))
|
||||
(check-type + : (→ Int Num Num))
|
||||
(check-type + : (→ Int Int Num))
|
||||
(check-not-type + : (→ Top Int Num))
|
||||
(check-not-type + : (→ Top Int Int))
|
||||
(check-type + : (→ Nat Int Top))
|
||||
|
||||
;; previous tests -------------------------------------------------------------
|
||||
;; some change due to more specific types
|
||||
(check-type 1 : Int)
|
||||
(check-not-type 1 : (→ Int Int))
|
||||
(check-type "one" : String)
|
||||
(check-type #f : Bool)
|
||||
(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 : Sym]) x) 1)) ; Sym is not valid type
|
||||
(typecheck-fail (λ ([x : Sym]) x)) ; Sym 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)
|
||||
;; changed test
|
||||
(check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 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) : Num ⇒ 20)
|
||||
|
||||
(check-not-type (λ ([x : Int]) x) : Int)
|
||||
(check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int))
|
||||
(check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))
|
||||
76
macrotypes/examples/tests/sysf-tests.rkt
Normal file
76
macrotypes/examples/tests/sysf-tests.rkt
Normal file
|
|
@ -0,0 +1,76 @@
|
|||
#lang s-exp "../sysf.rkt"
|
||||
(require "rackunit-typechecking.rkt")
|
||||
|
||||
(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 (Λ (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-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))
|
||||
|
||||
;; inst err
|
||||
(typecheck-fail
|
||||
(inst 1 Int)
|
||||
#:with-msg
|
||||
"Expected ∀ type, got: 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)
|
||||
|
||||
; ∀ errs
|
||||
(typecheck-fail (λ ([x : (∀ (y) (+ 1 y))]) x))
|
||||
|
||||
;; previous tests -------------------------------------------------------------
|
||||
(check-type 1 : Int)
|
||||
(check-not-type 1 : (→ Int Int))
|
||||
(typecheck-fail "one") ; unsupported literal
|
||||
(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)
|
||||
Loading…
Reference in New Issue
Block a user