diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/test/test/lux/meta/type/check.lux | 59 |
1 files changed, 31 insertions, 28 deletions
diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux index b1239fa43..127e02cbd 100644 --- a/stdlib/test/test/lux/meta/type/check.lux +++ b/stdlib/test/test/lux/meta/type/check.lux @@ -76,7 +76,7 @@ false)) ## [Tests] -(context: "Top and Bottom" +(context: "Top and Bottom." (<| (times +100) (do @ [sample (|> gen-type (r;filter valid-type?))] @@ -96,35 +96,35 @@ (test "Existential types only match with themselves." (and (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check ex ex))) + [[_ exT] @;existential] + (@;check exT exT))) (not (type-checks? (do @;Monad<Check> - [[lid lex] @;existential - [rid rex] @;existential] - (@;check lex rex)))))) + [[_ exTL] @;existential + [_ exTR] @;existential] + (@;check exTL exTR)))))) - (test "Names don't affect type-checking." + (test "Names do not affect type-checking." (and (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check (#;Named ["module" "name"] ex) - ex))) + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + exT))) (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check ex - (#;Named ["module" "name"] ex)))) + [[_ exT] @;existential] + (@;check exT + (#;Named ["module" "name"] exT)))) (type-checks? (do @;Monad<Check> - [[id ex] @;existential] - (@;check (#;Named ["module" "name"] ex) - (#;Named ["module" "name"] ex)))))) + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + (#;Named ["module" "name"] exT)))))) - (test "Can type-check functions." + (test "Functions are covariant on inputs and contravariant on outputs." (and (@;checks? (#;Function Bottom Top) (#;Function Top Bottom)) (not (@;checks? (#;Function Top Bottom) (#;Function Bottom Top))))) )) -(context: "Type application" +(context: "Type application." (<| (times +100) (do @ [meta gen-type @@ -135,7 +135,7 @@ (@;checks? (type;tuple (list meta data)) (|> Ann (#;Apply meta) (#;Apply data)))))))) -(context: "Primitive types" +(context: "Primitive types." (<| (times +100) (do @ [nameL gen-name @@ -156,7 +156,7 @@ (#;Primitive nameL (list paramR))))) )))) -(context: "Type-vars" +(context: "Type variables." ($_ seq (test "Type-vars check against themselves." (type-checks? (do @;Monad<Check> @@ -203,11 +203,11 @@ ids+types)] (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) -(context: "Rings." +(context: "Rings of type variables." (<| (times +100) (do @ [num-connections (|> r;nat (:: @ map (n.% +100))) - bound (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) + boundT (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) pick-pcg (r;seq r;nat r;nat)] ($_ seq (test "Can create rings of variables." @@ -227,26 +227,29 @@ same-vars?)))))) (test "When a var in a ring is bound, all the ring is bound." (type-checks? (do @;Monad<Check> - [[[head-id head-type] ids+types tail-type] (build-ring num-connections) + [[[head-id headT] ids+types tailT] (build-ring num-connections) #let [ids (list/map product;left ids+types)] - _ (@;check head-type bound) + _ (@;check headT boundT) head-bound (@;read head-id) tail-bound (monad;map @ @;read ids) headR (@;ring head-id) tailR+ (monad;map @ @;ring ids)] (let [rings-were-erased? (and (set;empty? headR) (list;every? set;empty? tailR+)) - same-types? (list;every? (type/= bound) (list& head-bound tail-bound))] + same-types? (list;every? (type/= boundT) (list& (maybe;default headT head-bound) + (list/map (function [[tail-id ?tailT]] + (maybe;default (#;Var tail-id) ?tailT)) + (list;zip2 ids tail-bound))))] (@;assert "" (and rings-were-erased? same-types?)))))) (test "Can merge multiple rings of variables." (type-checks? (do @;Monad<Check> - [[[head-idL head-typeL] ids+typesL [tail-idL tail-typeL]] (build-ring num-connections) - [[head-idR head-typeR] ids+typesR [tail-idR tail-typeR]] (build-ring num-connections) + [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections) + [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections) headRL-pre (@;ring head-idL) headRR-pre (@;ring head-idR) - _ (@;check head-typeL head-typeR) + _ (@;check headTL headTR) headRL-post (@;ring head-idL) headRR-post (@;ring head-idR)] (@;assert "" |