From e550029ac3ca8eecade4705020b9cf24312227f5 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sat, 21 Jul 2018 00:49:34 -0400 Subject: Moved "lux/language/type/*" to "lux/type/*". --- .../test/lux/language/compiler/analysis/case.lux | 4 +- .../lux/language/compiler/analysis/function.lux | 2 +- .../lux/language/compiler/analysis/primitive.lux | 2 +- .../compiler/analysis/procedure/common.lux | 2 +- .../lux/language/compiler/analysis/reference.lux | 5 +- .../lux/language/compiler/analysis/structure.lux | 4 +- stdlib/test/test/lux/language/type.lux | 166 ------------- stdlib/test/test/lux/language/type/check.lux | 265 --------------------- stdlib/test/test/lux/math/modular.lux | 3 +- stdlib/test/test/lux/type.lux | 165 +++++++++++++ stdlib/test/test/lux/type/check.lux | 264 ++++++++++++++++++++ stdlib/test/tests.lux | 5 +- 12 files changed, 441 insertions(+), 446 deletions(-) delete mode 100644 stdlib/test/test/lux/language/type.lux delete mode 100644 stdlib/test/test/lux/language/type/check.lux create mode 100644 stdlib/test/test/lux/type.lux create mode 100644 stdlib/test/test/lux/type/check.lux (limited to 'stdlib/test') diff --git a/stdlib/test/test/lux/language/compiler/analysis/case.lux b/stdlib/test/test/lux/language/compiler/analysis/case.lux index 183ae7da7..5956cc48e 100644 --- a/stdlib/test/test/lux/language/compiler/analysis/case.lux +++ b/stdlib/test/test/lux/language/compiler/analysis/case.lux @@ -12,11 +12,11 @@ ["." set]]] [math ["r" random ("random/." Monad)]] + ["." type + ["." check]] [macro ["." code]] [language - ["." type - ["." check]] ["." compiler ["." analysis ["." module] diff --git a/stdlib/test/test/lux/language/compiler/analysis/function.lux b/stdlib/test/test/lux/language/compiler/analysis/function.lux index 559a4a841..22ff04213 100644 --- a/stdlib/test/test/lux/language/compiler/analysis/function.lux +++ b/stdlib/test/test/lux/language/compiler/analysis/function.lux @@ -13,10 +13,10 @@ ["." list ("list/." Functor)]]] [math ["r" random]] + ["." type] ["." macro ["." code]] ["." language - ["." type] ["." reference] ["." compiler ["." init] diff --git a/stdlib/test/test/lux/language/compiler/analysis/primitive.lux b/stdlib/test/test/lux/language/compiler/analysis/primitive.lux index e49284c1a..adad90f18 100644 --- a/stdlib/test/test/lux/language/compiler/analysis/primitive.lux +++ b/stdlib/test/test/lux/language/compiler/analysis/primitive.lux @@ -10,10 +10,10 @@ format]] [math ["r" random ("random/." Monad)]] + [".L" type ("type/." Equivalence)] [macro ["." code]] ["." language - [".L" type ("type/." Equivalence)] ["." compiler ["." init] ["." analysis (#+ Analysis Operation) diff --git a/stdlib/test/test/lux/language/compiler/analysis/procedure/common.lux b/stdlib/test/test/lux/language/compiler/analysis/procedure/common.lux index 92afb7083..2a5cc2ee3 100644 --- a/stdlib/test/test/lux/language/compiler/analysis/procedure/common.lux +++ b/stdlib/test/test/lux/language/compiler/analysis/procedure/common.lux @@ -13,10 +13,10 @@ format]] [math ["r" random]] + [type ("type/." Equivalence)] [macro ["." code]] [language - [type ("type/." Equivalence)] ["." compiler ["." init] [analysis diff --git a/stdlib/test/test/lux/language/compiler/analysis/reference.lux b/stdlib/test/test/lux/language/compiler/analysis/reference.lux index ac302db3e..66c990ef4 100644 --- a/stdlib/test/test/lux/language/compiler/analysis/reference.lux +++ b/stdlib/test/test/lux/language/compiler/analysis/reference.lux @@ -9,11 +9,10 @@ [text ("text/." Equivalence)]] [math ["r" random]] + [type ("type/." Equivalence)] [macro ["." code]] - ["." language] - [language - [type ("type/." Equivalence)] + ["." language ["." reference] ["." compiler ["." init] diff --git a/stdlib/test/test/lux/language/compiler/analysis/structure.lux b/stdlib/test/test/lux/language/compiler/analysis/structure.lux index c3c5a0dc2..6dca4fb12 100644 --- a/stdlib/test/test/lux/language/compiler/analysis/structure.lux +++ b/stdlib/test/test/lux/language/compiler/analysis/structure.lux @@ -14,11 +14,11 @@ ["." set]]] [math ["r" random]] + ["." type ("type/." Equivalence) + ["." check]] [macro ["." code]] ["." language - ["." type ("type/." Equivalence) - ["." check]] ["." compiler ["." init] ["." analysis (#+ Analysis Variant Tag Operation) diff --git a/stdlib/test/test/lux/language/type.lux b/stdlib/test/test/lux/language/type.lux deleted file mode 100644 index 8db1c5a19..000000000 --- a/stdlib/test/test/lux/language/type.lux +++ /dev/null @@ -1,166 +0,0 @@ -(.module: - [lux #* - [control - ["M" monad (#+ do Monad)] - pipe] - [data - ["." maybe] - [text - format] - [collection - ["." list]]] - [math - ["r" random]] - [language - ["&" type]]] - lux/test) - -## [Utils] -(def: gen-name - (r.Random Text) - (do r.Monad - [size (|> r.nat (:: @ map (n/% +10)))] - (r.unicode size))) - -(def: gen-ident - (r.Random Ident) - (r.seq gen-name gen-name)) - -(def: gen-type - (r.Random Type) - (let [(^open "R/.") r.Monad] - (r.rec (function (_ gen-type) - ($_ r.alt - (r.seq gen-name (R/wrap (list))) - (r.seq gen-type gen-type) - (r.seq gen-type gen-type) - (r.seq gen-type gen-type) - r.nat - r.nat - r.nat - (r.seq (R/wrap (list)) gen-type) - (r.seq (R/wrap (list)) gen-type) - (r.seq gen-type gen-type) - (r.seq gen-ident gen-type) - ))))) - -## [Tests] -(context: "Types" - (<| (times +100) - (do @ - [sample gen-type] - (test "Every type is equal to itself." - (:: &.Equivalence = sample sample))))) - -(context: "Type application" - (test "Can apply quantified types (universal and existential quantification)." - (and (maybe.default #0 - (do maybe.Monad - [partial (&.apply (list Bit) Ann) - full (&.apply (list Int) partial)] - (wrap (:: &.Equivalence = full (#.Product Bit Int))))) - (|> (&.apply (list Bit) Text) - (case> #.None #1 _ #0))))) - -(context: "Naming" - (let [base (#.Named ["" "a"] (#.Product Bit Int)) - aliased (#.Named ["" "c"] - (#.Named ["" "b"] - base))] - ($_ seq - (test "Can remove aliases from an already-named type." - (:: &.Equivalence = - base - (&.un-alias aliased))) - - (test "Can remove all names from a type." - (and (not (:: &.Equivalence = - base - (&.un-name aliased))) - (:: &.Equivalence = - (&.un-name base) - (&.un-name aliased))))))) - -(context: "Type construction [structs]" - (<| (times +100) - (do @ - [size (|> r.nat (:: @ map (n/% +3))) - members (|> gen-type - (r.filter (function (_ type) - (case type - (^or (#.Sum _) (#.Product _)) - #0 - - _ - #1))) - (list.repeat size) - (M.seq @)) - #let [(^open "&/.") &.Equivalence - (^open "L/.") (list.Equivalence &.Equivalence)]] - (with-expansions - [ (do-template [ ] - [(test (format "Can build and tear-down " " types.") - (let [flat (|> members )] - (or (L/= members flat) - (and (L/= (list) members) - (L/= (list ) flat)))))] - - ["variant" &.variant &.flatten-variant Nothing] - ["tuple" &.tuple &.flatten-tuple Any] - )] - ($_ seq - - ))))) - -(context: "Type construction [parameterized]" - (<| (times +100) - (do @ - [size (|> r.nat (:: @ map (n/% +3))) - members (M.seq @ (list.repeat size gen-type)) - extra (|> gen-type - (r.filter (function (_ type) - (case type - (^or (#.Function _) (#.Apply _)) - #0 - - _ - #1)))) - #let [(^open "&/.") &.Equivalence - (^open "L/.") (list.Equivalence &.Equivalence)]] - ($_ seq - (test "Can build and tear-down function types." - (let [[inputs output] (|> (&.function members extra) &.flatten-function)] - (and (L/= members inputs) - (&/= extra output)))) - - (test "Can build and tear-down application types." - (let [[tfunc tparams] (|> extra (&.application members) &.flatten-application)] - (n/= (list.size members) (list.size tparams)))) - )))) - -(context: "Type construction [higher order]" - (<| (times +100) - (do @ - [size (|> r.nat (:: @ map (n/% +3))) - extra (|> gen-type - (r.filter (function (_ type) - (case type - (^or (#.UnivQ _) (#.ExQ _)) - #0 - - _ - #1)))) - #let [(^open "&/.") &.Equivalence]] - (with-expansions - [ (do-template [ ] - [(test (format "Can build and tear-down " " types.") - (let [[flat-size flat-body] (|> extra ( size) )] - (and (n/= size flat-size) - (&/= extra flat-body))))] - - ["universally-quantified" &.univ-q &.flatten-univ-q] - ["existentially-quantified" &.ex-q &.flatten-ex-q] - )] - ($_ seq - - ))))) diff --git a/stdlib/test/test/lux/language/type/check.lux b/stdlib/test/test/lux/language/type/check.lux deleted file mode 100644 index a8cf1963f..000000000 --- a/stdlib/test/test/lux/language/type/check.lux +++ /dev/null @@ -1,265 +0,0 @@ -(.module: - [lux #* - [control - ["." monad (#+ do Monad)] - [pipe (#+ case>)]] - [data - ["." product] - ["." maybe] - ["." number] - [text ("text/." Equivalence)] - [collection - ["." list ("list/." Functor)] - ["." set]]] - [math - ["r" random]] - [language - ["." type ("type/." Equivalence) - ["@" check]]]] - lux/test) - -## [Utils] -(def: gen-name - (r.Random Text) - (do r.Monad - [size (|> r.nat (:: @ map (n/% +10)))] - (r.unicode size))) - -(def: gen-ident - (r.Random Ident) - (r.seq gen-name gen-name)) - -(def: gen-type - (r.Random Type) - (let [(^open "r/.") r.Monad] - (r.rec (function (_ gen-type) - ($_ r.alt - (r.seq gen-name (r/wrap (list))) - (r.seq gen-type gen-type) - (r.seq gen-type gen-type) - (r.seq gen-type gen-type) - r.nat - r.nat - r.nat - (r.seq (r/wrap (list)) gen-type) - (r.seq (r/wrap (list)) gen-type) - (r.seq gen-type gen-type) - (r.seq gen-ident gen-type) - ))))) - -(def: (valid-type? type) - (-> Type Bit) - (case type - (#.Primitive name params) - (list.every? valid-type? params) - - (#.Ex id) - #1 - - (^template [] - ( left right) - (and (valid-type? left) (valid-type? right))) - ([#.Sum] [#.Product] [#.Function]) - - (#.Named name type') - (valid-type? type') - - _ - #0)) - -(def: (type-checks? input) - (-> (@.Check []) Bit) - (case (@.run @.fresh-context input) - (#.Right []) - #1 - - (#.Left error) - #0)) - -## [Tests] -(context: "Any and Nothing." - (<| (times +100) - (do @ - [sample (|> gen-type (r.filter valid-type?))] - ($_ seq - (test "Any is the super-type of everything." - (@.checks? Any sample)) - - (test "Nothing is the sub-type of everything." - (@.checks? sample Nothing)) - )))) - -(context: "Simple type-checking." - ($_ seq - (test "Any and Nothing match themselves." - (and (@.checks? Nothing Nothing) - (@.checks? Any Any))) - - (test "Existential types only match with themselves." - (and (type-checks? (do @.Monad - [[_ exT] @.existential] - (@.check exT exT))) - (not (type-checks? (do @.Monad - [[_ exTL] @.existential - [_ exTR] @.existential] - (@.check exTL exTR)))))) - - (test "Names do not affect type-checking." - (and (type-checks? (do @.Monad - [[_ exT] @.existential] - (@.check (#.Named ["module" "name"] exT) - exT))) - (type-checks? (do @.Monad - [[_ exT] @.existential] - (@.check exT - (#.Named ["module" "name"] exT)))) - (type-checks? (do @.Monad - [[_ exT] @.existential] - (@.check (#.Named ["module" "name"] exT) - (#.Named ["module" "name"] exT)))))) - - (test "Functions are covariant on inputs and contravariant on outputs." - (and (@.checks? (#.Function Nothing Any) - (#.Function Any Nothing)) - (not (@.checks? (#.Function Any Nothing) - (#.Function Nothing Any))))) - )) - -(context: "Type application." - (<| (times +100) - (do @ - [meta gen-type - data gen-type] - (test "Can type-check type application." - (and (@.checks? (|> Ann (#.Apply meta) (#.Apply data)) - (type.tuple (list meta data))) - (@.checks? (type.tuple (list meta data)) - (|> Ann (#.Apply meta) (#.Apply data)))))))) - -(context: "Primitive types." - (<| (times +100) - (do @ - [nameL gen-name - nameR (|> gen-name (r.filter (|>> (text/= nameL) not))) - paramL gen-type - paramR (|> gen-type (r.filter (|>> (@.checks? paramL) not)))] - ($_ seq - (test "Primitive types match when they have the same name and the same parameters." - (@.checks? (#.Primitive nameL (list paramL)) - (#.Primitive nameL (list paramL)))) - - (test "Names matter to primitive types." - (not (@.checks? (#.Primitive nameL (list paramL)) - (#.Primitive nameR (list paramL))))) - - (test "Parameters matter to primitive types." - (not (@.checks? (#.Primitive nameL (list paramL)) - (#.Primitive nameL (list paramR))))) - )))) - -(context: "Type variables." - ($_ seq - (test "Type-vars check against themselves." - (type-checks? (do @.Monad - [[id var] @.var] - (@.check var var)))) - - (test "Can bind unbound type-vars by type-checking against them." - (and (type-checks? (do @.Monad - [[id var] @.var] - (@.check var .Any))) - (type-checks? (do @.Monad - [[id var] @.var] - (@.check .Any var))))) - - (test "Cannot rebind already bound type-vars." - (not (type-checks? (do @.Monad - [[id var] @.var - _ (@.check var .Bit)] - (@.check var .Nat))))) - - (test "If the type bound to a var is a super-type to another, then the var is also a super-type." - (type-checks? (do @.Monad - [[id var] @.var - _ (@.check var Any)] - (@.check var .Bit)))) - - (test "If the type bound to a var is a sub-type of another, then the var is also a sub-type." - (type-checks? (do @.Monad - [[id var] @.var - _ (@.check var Nothing)] - (@.check .Bit var)))) - )) - -(def: (build-ring num-connections) - (-> Nat (@.Check [[Nat Type] (List [Nat Type]) [Nat Type]])) - (do @.Monad - [[head-id head-type] @.var - ids+types (monad.seq @ (list.repeat num-connections @.var)) - [tail-id tail-type] (monad.fold @ (function (_ [tail-id tail-type] [_head-id _head-type]) - (do @ - [_ (@.check head-type tail-type)] - (wrap [tail-id tail-type]))) - [head-id head-type] - ids+types)] - (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) - -(context: "Rings of type variables." - (<| (times +100) - (do @ - [num-connections (|> r.nat (:: @ map (n/% +100))) - boundT (|> gen-type (r.filter (|>> (case> (#.Var _) #0 _ #1)))) - pick-pcg (r.seq r.nat r.nat)] - ($_ seq - (test "Can create rings of variables." - (type-checks? (do @.Monad - [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections) - #let [ids (list/map product.left ids+types)] - headR (@.ring head-id) - tailR (@.ring tail-id)] - (@.assert "" - (let [same-rings? (:: set.Equivalence = headR tailR) - expected-size? (n/= (inc num-connections) (set.size headR)) - same-vars? (|> (set.to-list headR) - (list.sort n/<) - (:: (list.Equivalence number.Equivalence) = (list.sort n/< (#.Cons head-id ids))))] - (and same-rings? - expected-size? - same-vars?)))))) - (test "When a var in a ring is bound, all the ring is bound." - (type-checks? (do @.Monad - [[[head-id headT] ids+types tailT] (build-ring num-connections) - #let [ids (list/map product.left ids+types)] - _ (@.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/= 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 - [[[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 headTL headTR) - headRL-post (@.ring head-idL) - headRR-post (@.ring head-idR)] - (@.assert "" - (let [same-rings? (:: set.Equivalence = headRL-post headRR-post) - expected-size? (n/= (n/* +2 (inc num-connections)) - (set.size headRL-post)) - union? (:: set.Equivalence = headRL-post (set.union headRL-pre headRR-pre))] - (and same-rings? - expected-size? - union?)))))) - )) - )) diff --git a/stdlib/test/test/lux/math/modular.lux b/stdlib/test/test/lux/math/modular.lux index cd1f637e9..ad9fda295 100644 --- a/stdlib/test/test/lux/math/modular.lux +++ b/stdlib/test/test/lux/math/modular.lux @@ -11,8 +11,7 @@ [math ["r" random] ["/" modular]] - [language - [type ("type/." Equivalence)]]] + [type ("type/." Equivalence)]] lux/test) (def: %3 (/.modulus 3)) diff --git a/stdlib/test/test/lux/type.lux b/stdlib/test/test/lux/type.lux new file mode 100644 index 000000000..9592170ff --- /dev/null +++ b/stdlib/test/test/lux/type.lux @@ -0,0 +1,165 @@ +(.module: + [lux #* + [control + ["M" monad (#+ do Monad)] + pipe] + [data + ["." maybe] + [text + format] + [collection + ["." list]]] + [math + ["r" random]] + ["&" type]] + lux/test) + +## [Utils] +(def: gen-name + (r.Random Text) + (do r.Monad + [size (|> r.nat (:: @ map (n/% +10)))] + (r.unicode size))) + +(def: gen-ident + (r.Random Ident) + (r.seq gen-name gen-name)) + +(def: gen-type + (r.Random Type) + (let [(^open "R/.") r.Monad] + (r.rec (function (_ gen-type) + ($_ r.alt + (r.seq gen-name (R/wrap (list))) + (r.seq gen-type gen-type) + (r.seq gen-type gen-type) + (r.seq gen-type gen-type) + r.nat + r.nat + r.nat + (r.seq (R/wrap (list)) gen-type) + (r.seq (R/wrap (list)) gen-type) + (r.seq gen-type gen-type) + (r.seq gen-ident gen-type) + ))))) + +## [Tests] +(context: "Types" + (<| (times +100) + (do @ + [sample gen-type] + (test "Every type is equal to itself." + (:: &.Equivalence = sample sample))))) + +(context: "Type application" + (test "Can apply quantified types (universal and existential quantification)." + (and (maybe.default #0 + (do maybe.Monad + [partial (&.apply (list Bit) Ann) + full (&.apply (list Int) partial)] + (wrap (:: &.Equivalence = full (#.Product Bit Int))))) + (|> (&.apply (list Bit) Text) + (case> #.None #1 _ #0))))) + +(context: "Naming" + (let [base (#.Named ["" "a"] (#.Product Bit Int)) + aliased (#.Named ["" "c"] + (#.Named ["" "b"] + base))] + ($_ seq + (test "Can remove aliases from an already-named type." + (:: &.Equivalence = + base + (&.un-alias aliased))) + + (test "Can remove all names from a type." + (and (not (:: &.Equivalence = + base + (&.un-name aliased))) + (:: &.Equivalence = + (&.un-name base) + (&.un-name aliased))))))) + +(context: "Type construction [structs]" + (<| (times +100) + (do @ + [size (|> r.nat (:: @ map (n/% +3))) + members (|> gen-type + (r.filter (function (_ type) + (case type + (^or (#.Sum _) (#.Product _)) + #0 + + _ + #1))) + (list.repeat size) + (M.seq @)) + #let [(^open "&/.") &.Equivalence + (^open "L/.") (list.Equivalence &.Equivalence)]] + (with-expansions + [ (do-template [ ] + [(test (format "Can build and tear-down " " types.") + (let [flat (|> members )] + (or (L/= members flat) + (and (L/= (list) members) + (L/= (list ) flat)))))] + + ["variant" &.variant &.flatten-variant Nothing] + ["tuple" &.tuple &.flatten-tuple Any] + )] + ($_ seq + + ))))) + +(context: "Type construction [parameterized]" + (<| (times +100) + (do @ + [size (|> r.nat (:: @ map (n/% +3))) + members (M.seq @ (list.repeat size gen-type)) + extra (|> gen-type + (r.filter (function (_ type) + (case type + (^or (#.Function _) (#.Apply _)) + #0 + + _ + #1)))) + #let [(^open "&/.") &.Equivalence + (^open "L/.") (list.Equivalence &.Equivalence)]] + ($_ seq + (test "Can build and tear-down function types." + (let [[inputs output] (|> (&.function members extra) &.flatten-function)] + (and (L/= members inputs) + (&/= extra output)))) + + (test "Can build and tear-down application types." + (let [[tfunc tparams] (|> extra (&.application members) &.flatten-application)] + (n/= (list.size members) (list.size tparams)))) + )))) + +(context: "Type construction [higher order]" + (<| (times +100) + (do @ + [size (|> r.nat (:: @ map (n/% +3))) + extra (|> gen-type + (r.filter (function (_ type) + (case type + (^or (#.UnivQ _) (#.ExQ _)) + #0 + + _ + #1)))) + #let [(^open "&/.") &.Equivalence]] + (with-expansions + [ (do-template [ ] + [(test (format "Can build and tear-down " " types.") + (let [[flat-size flat-body] (|> extra ( size) )] + (and (n/= size flat-size) + (&/= extra flat-body))))] + + ["universally-quantified" &.univ-q &.flatten-univ-q] + ["existentially-quantified" &.ex-q &.flatten-ex-q] + )] + ($_ seq + + ))))) diff --git a/stdlib/test/test/lux/type/check.lux b/stdlib/test/test/lux/type/check.lux new file mode 100644 index 000000000..c817ec61e --- /dev/null +++ b/stdlib/test/test/lux/type/check.lux @@ -0,0 +1,264 @@ +(.module: + [lux #* + [control + ["." monad (#+ do Monad)] + [pipe (#+ case>)]] + [data + ["." product] + ["." maybe] + ["." number] + [text ("text/." Equivalence)] + [collection + ["." list ("list/." Functor)] + ["." set]]] + [math + ["r" random]] + ["." type ("type/." Equivalence) + ["@" check]]] + lux/test) + +## [Utils] +(def: gen-name + (r.Random Text) + (do r.Monad + [size (|> r.nat (:: @ map (n/% +10)))] + (r.unicode size))) + +(def: gen-ident + (r.Random Ident) + (r.seq gen-name gen-name)) + +(def: gen-type + (r.Random Type) + (let [(^open "r/.") r.Monad] + (r.rec (function (_ gen-type) + ($_ r.alt + (r.seq gen-name (r/wrap (list))) + (r.seq gen-type gen-type) + (r.seq gen-type gen-type) + (r.seq gen-type gen-type) + r.nat + r.nat + r.nat + (r.seq (r/wrap (list)) gen-type) + (r.seq (r/wrap (list)) gen-type) + (r.seq gen-type gen-type) + (r.seq gen-ident gen-type) + ))))) + +(def: (valid-type? type) + (-> Type Bit) + (case type + (#.Primitive name params) + (list.every? valid-type? params) + + (#.Ex id) + #1 + + (^template [] + ( left right) + (and (valid-type? left) (valid-type? right))) + ([#.Sum] [#.Product] [#.Function]) + + (#.Named name type') + (valid-type? type') + + _ + #0)) + +(def: (type-checks? input) + (-> (@.Check []) Bit) + (case (@.run @.fresh-context input) + (#.Right []) + #1 + + (#.Left error) + #0)) + +## [Tests] +(context: "Any and Nothing." + (<| (times +100) + (do @ + [sample (|> gen-type (r.filter valid-type?))] + ($_ seq + (test "Any is the super-type of everything." + (@.checks? Any sample)) + + (test "Nothing is the sub-type of everything." + (@.checks? sample Nothing)) + )))) + +(context: "Simple type-checking." + ($_ seq + (test "Any and Nothing match themselves." + (and (@.checks? Nothing Nothing) + (@.checks? Any Any))) + + (test "Existential types only match with themselves." + (and (type-checks? (do @.Monad + [[_ exT] @.existential] + (@.check exT exT))) + (not (type-checks? (do @.Monad + [[_ exTL] @.existential + [_ exTR] @.existential] + (@.check exTL exTR)))))) + + (test "Names do not affect type-checking." + (and (type-checks? (do @.Monad + [[_ exT] @.existential] + (@.check (#.Named ["module" "name"] exT) + exT))) + (type-checks? (do @.Monad + [[_ exT] @.existential] + (@.check exT + (#.Named ["module" "name"] exT)))) + (type-checks? (do @.Monad + [[_ exT] @.existential] + (@.check (#.Named ["module" "name"] exT) + (#.Named ["module" "name"] exT)))))) + + (test "Functions are covariant on inputs and contravariant on outputs." + (and (@.checks? (#.Function Nothing Any) + (#.Function Any Nothing)) + (not (@.checks? (#.Function Any Nothing) + (#.Function Nothing Any))))) + )) + +(context: "Type application." + (<| (times +100) + (do @ + [meta gen-type + data gen-type] + (test "Can type-check type application." + (and (@.checks? (|> Ann (#.Apply meta) (#.Apply data)) + (type.tuple (list meta data))) + (@.checks? (type.tuple (list meta data)) + (|> Ann (#.Apply meta) (#.Apply data)))))))) + +(context: "Primitive types." + (<| (times +100) + (do @ + [nameL gen-name + nameR (|> gen-name (r.filter (|>> (text/= nameL) not))) + paramL gen-type + paramR (|> gen-type (r.filter (|>> (@.checks? paramL) not)))] + ($_ seq + (test "Primitive types match when they have the same name and the same parameters." + (@.checks? (#.Primitive nameL (list paramL)) + (#.Primitive nameL (list paramL)))) + + (test "Names matter to primitive types." + (not (@.checks? (#.Primitive nameL (list paramL)) + (#.Primitive nameR (list paramL))))) + + (test "Parameters matter to primitive types." + (not (@.checks? (#.Primitive nameL (list paramL)) + (#.Primitive nameL (list paramR))))) + )))) + +(context: "Type variables." + ($_ seq + (test "Type-vars check against themselves." + (type-checks? (do @.Monad + [[id var] @.var] + (@.check var var)))) + + (test "Can bind unbound type-vars by type-checking against them." + (and (type-checks? (do @.Monad + [[id var] @.var] + (@.check var .Any))) + (type-checks? (do @.Monad + [[id var] @.var] + (@.check .Any var))))) + + (test "Cannot rebind already bound type-vars." + (not (type-checks? (do @.Monad + [[id var] @.var + _ (@.check var .Bit)] + (@.check var .Nat))))) + + (test "If the type bound to a var is a super-type to another, then the var is also a super-type." + (type-checks? (do @.Monad + [[id var] @.var + _ (@.check var Any)] + (@.check var .Bit)))) + + (test "If the type bound to a var is a sub-type of another, then the var is also a sub-type." + (type-checks? (do @.Monad + [[id var] @.var + _ (@.check var Nothing)] + (@.check .Bit var)))) + )) + +(def: (build-ring num-connections) + (-> Nat (@.Check [[Nat Type] (List [Nat Type]) [Nat Type]])) + (do @.Monad + [[head-id head-type] @.var + ids+types (monad.seq @ (list.repeat num-connections @.var)) + [tail-id tail-type] (monad.fold @ (function (_ [tail-id tail-type] [_head-id _head-type]) + (do @ + [_ (@.check head-type tail-type)] + (wrap [tail-id tail-type]))) + [head-id head-type] + ids+types)] + (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) + +(context: "Rings of type variables." + (<| (times +100) + (do @ + [num-connections (|> r.nat (:: @ map (n/% +100))) + boundT (|> gen-type (r.filter (|>> (case> (#.Var _) #0 _ #1)))) + pick-pcg (r.seq r.nat r.nat)] + ($_ seq + (test "Can create rings of variables." + (type-checks? (do @.Monad + [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections) + #let [ids (list/map product.left ids+types)] + headR (@.ring head-id) + tailR (@.ring tail-id)] + (@.assert "" + (let [same-rings? (:: set.Equivalence = headR tailR) + expected-size? (n/= (inc num-connections) (set.size headR)) + same-vars? (|> (set.to-list headR) + (list.sort n/<) + (:: (list.Equivalence number.Equivalence) = (list.sort n/< (#.Cons head-id ids))))] + (and same-rings? + expected-size? + same-vars?)))))) + (test "When a var in a ring is bound, all the ring is bound." + (type-checks? (do @.Monad + [[[head-id headT] ids+types tailT] (build-ring num-connections) + #let [ids (list/map product.left ids+types)] + _ (@.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/= 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 + [[[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 headTL headTR) + headRL-post (@.ring head-idL) + headRR-post (@.ring head-idR)] + (@.assert "" + (let [same-rings? (:: set.Equivalence = headRL-post headRR-post) + expected-size? (n/= (n/* +2 (inc num-connections)) + (set.size headRL-post)) + union? (:: set.Equivalence = headRL-post (set.union headRL-pre headRR-pre))] + (and same-rings? + expected-size? + union?)))))) + )) + )) diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux index a795556eb..bdd8ef0ab 100644 --- a/stdlib/test/tests.lux +++ b/stdlib/test/tests.lux @@ -143,7 +143,8 @@ [poly ["poly_." equivalence] ["poly_." functor]]] - [type + ["_." type + ["_." check] ## ["_." implicit] ## TODO: Specially troublesome... ["_." resource] [object @@ -151,8 +152,6 @@ ["_." protocol]]] [language ["_language/." syntax] - ["_." type - ["_." check]] [compiler [analysis ["_.A" primitive] -- cgit v1.2.3