suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

convert more mlish tests to typed-lang-builder/mlish-core

Browse Source
This commit is contained in:
AlexKnauth 2016-06-22 16:58:40 -04:00
parent 3fac6b1bc3
commit 143bb714ce
3 changed files with 34 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tapl/tests/mlish/bg/okasaki.mlish
View File

@ -1,4 +1,4 @@
#lang s-exp "../../../mlish.rkt"
#lang s-exp "../../../typed-lang-builder/mlish-core.rkt"
(require "../../rackunit-typechecking.rkt")
;; TODO

64
tapl/tests/mlish/infer-variances.mlish
View File

@ -1,4 +1,4 @@
#lang s-exp "../../mlish.rkt"
#lang s-exp "../../typed-lang-builder/mlish-core.rkt"
(require "../rackunit-typechecking.rkt")
(define-type T1 t1)
@ -18,13 +18,13 @@
;; This checks that X is covariant within (T2 X).
(define (t2* → (T2 X)) t2)
(define (t2** → (→ (T2 X))) t2*)
(define (t2** → (→ (T2 X))) (inst t2* X))
(check-type (t2**) : (→/test (T2 X)))
;; This checks that X is contravariant within (T2 X),
;; by checking that X is covariant within (→ (T2 X) Int).
(define (t2->int [t2 : (T2 X)] → Int) 0)
(define (t2->int* → (→ (T2 X) Int)) t2->int)
(define (t2->int* → (→ (T2 X) Int)) (inst t2->int X))
(check-type (t2->int*) : (→/test (T2 X) Int))
;; This checks that X is irrelevant, even within a Ref type,
@ -32,7 +32,7 @@
;; This is still sound because a value of type (Ref (T2 X)) will never
;; contain anything of type X anyway. X is irrelevant within it.
(define (ref-t2* → (Ref (T2 X))) (ref (t2 {X})))
(define (ref-t2** → (→ (Ref (T2 X)))) ref-t2*)
(define (ref-t2** → (→ (Ref (T2 X)))) (inst ref-t2* X))
(check-type (ref-t2**) : (→/test (Ref (T2 X))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -42,13 +42,13 @@
;; This checks that X is covariant within (T3 X).
(define (t3-none* → (T3 X)) t3-none)
(define (t3-none** → (→ (T3 X))) t3-none*)
(define (t3-none** → (→ (T3 X))) (inst t3-none* X))
(check-type (t3-none**) : (→/test (T3 X)))
;; This checks that X is not contravariant within (T3 X),
;; by checking that X is not covariant within (→ (T3 X) Int).
(define (t3->int [t3 : (T3 X)] → Int) 0)
(define (t3->int* → (→ (T3 X) Int)) t3->int)
(define (t3->int* → (→ (T3 X) Int)) (inst t3->int X))
(typecheck-fail (t3->int*))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -58,13 +58,13 @@
;; This checks that X is not covariant within (T4 X).
(define (t4-none* → (T4 X)) t4-none)
(define (t4-none** → (→ (T4 X))) t4-none*)
(define (t4-none** → (→ (T4 X))) (inst t4-none* X))
(typecheck-fail (t4-none**))
;; This checks that X is contravariant within (T4 X),
;; by checking that X is covariant within (→ (T4 X) Int).
(define (t4->int [t4 : (T4 X)] → Int) 0)
(define (t4->int* → (→ (T4 X) Int)) t4->int)
(define (t4->int* → (→ (T4 X) Int)) (inst t4->int X))
(check-type (t4->int*) : (→/test (T4 X) Int))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -74,13 +74,13 @@
;; This checks that X is not covariant within (T5 X).
(define (t5-none* → (T5 X)) t5-none)
(define (t5-none** → (→ (T5 X))) t5-none*)
(define (t5-none** → (→ (T5 X))) (inst t5-none* X))
(typecheck-fail (t5-none**))
;; This checks that X is not contravariant within (T5 X),
;; by checking that X is not covariant within (→ (T5 X) Int).
(define (t5->int [t5 : (T5 X)] → Int) 0)
(define (t5->int* → (→ (T5 X) Int)) t5->int)
(define (t5->int* → (→ (T5 X) Int)) (inst t5->int X))
(typecheck-fail (t5->int*))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -94,13 +94,13 @@
;; This checks that X is covariant within (T6 X).
(define (t6-none* → (T6 X)) t6-none)
(define (t6-none** → (→ (T6 X))) t6-none*)
(define (t6-none** → (→ (T6 X))) (inst t6-none* X))
(check-type (t6-none**) : (→/test (T6 X)))
;; This checks that X is contravariant within (T6 X),
;; by checking that X is covariant within (→ (T6 X) Int).
(define (t6->int [t6 : (T6 X)] → Int) 0)
(define (t6->int* → (→ (T6 X) Int)) t6->int)
(define (t6->int* → (→ (T6 X) Int)) (inst t6->int X))
(check-type (t6->int*) : (→/test (T6 X) Int))
;; This checks that X is irrelevant, even within a Ref type,
@ -108,7 +108,7 @@
;; This is still sound because a value of type (Ref (T6 X)) will never
;; contain anything of type X anyway. X is irrelevant within it.
(define (ref-t6* → (Ref (T6 X))) (ref (t6-none {X})))
(define (ref-t6** → (→ (Ref (T6 X)))) ref-t6*)
(define (ref-t6** → (→ (Ref (T6 X)))) (inst ref-t6* X))
(check-type (ref-t6**) : (→/test (Ref (T6 X))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -124,13 +124,13 @@
;; This checks that X is covariant within (T10 X).
(define (t10-none* → (T10 X)) (t10 t7-none t8-none t9-none))
(define (t10-none** → (→ (T10 X))) t10-none*)
(define (t10-none** → (→ (T10 X))) (inst t10-none* X))
(check-type (t10-none**) : (→/test (T10 X)))
;; This checks that X is contravariant within (T10 X),
;; by checking that X is covariant within (→ (T10 X) Int).
(define (t10->int [t10 : (T10 X)] → Int) 0)
(define (t10->int* → (→ (T10 X) Int)) t10->int)
(define (t10->int* → (→ (T10 X) Int)) (inst t10->int X))
(check-type (t10->int*) : (→/test (T10 X) Int))
;; This checks that X is irrelevant, even within a Ref type,
@ -138,7 +138,7 @@
;; This is still sound because a value of type (Ref (T10 X)) will never
;; contain anything of type X anyway. X is irrelevant within it.
(define (ref-t10* → (Ref (T10 X))) (ref (t10 (t7-none {X}) (t8-none {X}) (t9-none {X}))))
(define (ref-t10** → (→ (Ref (T10 X)))) ref-t10*)
(define (ref-t10** → (→ (Ref (T10 X)))) (inst ref-t10* X))
(check-type (ref-t10**) : (→/test (Ref (T10 X))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -158,10 +158,10 @@
(define (t12-none* → (T12 X)) t12-none)
(define (t13-none* → (T13 X)) t13-none)
(define (t14-none* → (T14 X)) t14-none)
(define (t11-none** → (→ (T11 X))) t11-none*)
(define (t12-none** → (→ (T12 X))) t12-none*)
(define (t13-none** → (→ (T13 X))) t13-none*)
(define (t14-none** → (→ (T14 X))) t14-none*)
(define (t11-none** → (→ (T11 X))) (inst t11-none* X))
(define (t12-none** → (→ (T12 X))) (inst t12-none* X))
(define (t13-none** → (→ (T13 X))) (inst t13-none* X))
(define (t14-none** → (→ (T14 X))) (inst t14-none* X))
(typecheck-fail (t11-none**))
(typecheck-fail (t12-none**))
(check-type (t13-none**) : (→/test (T13 X)))
@ -173,10 +173,10 @@
(define (t12->int [t12 : (T12 X)] → Int) 0)
(define (t13->int [t13 : (T13 X)] → Int) 0)
(define (t14->int [t14 : (T14 X)] → Int) 0)
(define (t11->int* → (→ (T11 X) Int)) t11->int)
(define (t12->int* → (→ (T12 X) Int)) t12->int)
(define (t13->int* → (→ (T13 X) Int)) t13->int)
(define (t14->int* → (→ (T14 X) Int)) t14->int)
(define (t11->int* → (→ (T11 X) Int)) (inst t11->int X))
(define (t12->int* → (→ (T12 X) Int)) (inst t12->int X))
(define (t13->int* → (→ (T13 X) Int)) (inst t13->int X))
(define (t14->int* → (→ (T14 X) Int)) (inst t14->int X))
(typecheck-fail (t11->int*))
(typecheck-fail (t12->int*))
(typecheck-fail (t13->int*))
@ -192,22 +192,22 @@
;; This checks that X is covariant within (T15 X).
(define (t15-none* → (T15 X)) t15-none)
(define (t15-none** → (→ (T15 X))) t15-none*)
(define (t15-none** → (→ (T15 X))) (inst t15-none* X))
(check-type (t15-none**) : (→/test (T15 X)))
;; This checks that X is not covariant within (T16 X).
(define (t16-none* → (T16 X)) t16-none)
(define (t16-none** → (→ (T16 X))) t16-none*)
(define (t16-none** → (→ (T16 X))) (inst t16-none* X))
(typecheck-fail (t16-none**))
;; This checks that X is not contravariant within (T15 X),
;; by checking that X is not covariant within (→ (T15 X) Int).
(define (t15->int [t15 : (T15 X)] → Int) 0)
(define (t15->int* → (→ (T15 X) Int)) t15->int)
(define (t15->int* → (→ (T15 X) Int)) (inst t15->int X))
(typecheck-fail (t15->int*))
;; This checks that X is contravariant within (T16 X),
;; by checking that X is covariant within (→ (T16 X) Int).
(define (t16->int [t16 : (T16 X)] → Int) 0)
(define (t16->int* → (→ (T16 X) Int)) t16->int)
(define (t16->int* → (→ (T16 X) Int)) (inst t16->int X))
(check-type (t16->int*) : (→/test (T16 X) Int))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -223,21 +223,21 @@
;; This checks that X is covariant within (T17 X).
(define (t17-none* → (T17 X)) (t18 t18-none))
(define (t17-none** → (→ (T17 X))) t17-none*)
(define (t17-none** → (→ (T17 X))) (inst t17-none* X))
(check-type (t17-none**) : (→/test (T17 X)))
;; This checks that X is covariant within (T18 X).
(define (t18-none* → (T18 X)) t18-none)
(define (t18-none** → (→ (T18 X))) t18-none*)
(define (t18-none** → (→ (T18 X))) (inst t18-none* X))
(check-type (t18-none**) : (→/test (T18 X)))
;; This checks that X is not contravariant within (T17 X),
;; by checking that X is not covariant within (→ (T17 X) Int).
(define (t17->int [t17 : (T17 X)] → Int) 0)
(define (t17->int* → (→ (T17 X) Int)) t17->int)
(define (t17->int* → (→ (T17 X) Int)) (inst t17->int X))
(typecheck-fail (t17->int*))
;; This checks that X is not contravariant within (T18 X),
;; by checking that X is not covariant within (→ (T18 X) Int).
(define (t18->int [t18 : (T18 X)] → Int) 0)
(define (t18->int* → (→ (T18 X) Int)) t18->int)
(define (t18->int* → (→ (T18 X) Int)) (inst t18->int X))
(typecheck-fail (t18->int*))

2
tapl/tests/mlish/sweet-map.rkt
View File

@ -1,4 +1,4 @@
#lang sweet-exp "../../mlish.rkt"
#lang sweet-exp "../../typed-lang-builder/mlish-core.rkt"
define
sum [lst : (List Int)] → Int