diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/lux/type/implicit.lux | 44 | ||||
| -rw-r--r-- | stdlib/source/lux/type/resource.lux | 20 | ||||
| -rw-r--r-- | stdlib/source/test/lux.lux | 14 | ||||
| -rw-r--r-- | stdlib/source/test/lux/macro/poly/equivalence.lux | 2 | ||||
| -rw-r--r-- | stdlib/source/test/lux/type.lux | 287 | ||||
| -rw-r--r-- | stdlib/source/test/lux/type/check.lux | 395 | ||||
| -rw-r--r-- | stdlib/source/test/lux/type/dynamic.lux | 55 | ||||
| -rw-r--r-- | stdlib/source/test/lux/type/implicit.lux | 65 | ||||
| -rw-r--r-- | stdlib/source/test/lux/type/resource.lux | 84 |
9 files changed, 484 insertions, 482 deletions
diff --git a/stdlib/source/lux/type/implicit.lux b/stdlib/source/lux/type/implicit.lux index 1161a45b3..36d9b2e03 100644 --- a/stdlib/source/lux/type/implicit.lux +++ b/stdlib/source/lux/type/implicit.lux @@ -8,10 +8,10 @@ ["." product] ["." maybe] ["." number] - ["." text ("#;." equivalence) + ["." text ("#@." equivalence) format] [collection - ["." list ("#;." monad fold)] + ["." list ("#@." monad fold)] ["dict" dictionary (#+ Dictionary)]]] ["." macro ["." code] @@ -86,8 +86,8 @@ [this-module-name macro.current-module-name imp-mods (macro.imported-modules this-module-name) tag-lists (monad.map @ macro.tag-lists imp-mods) - #let [tag-lists (|> tag-lists list;join (list;map product.left) list;join) - candidates (list.filter (|>> product.right (text;= simple-name)) + #let [tag-lists (|> tag-lists list@join (list@map product.left) list@join) + candidates (list.filter (|>> product.right (text@= simple-name)) tag-lists)]] (case candidates #.Nil @@ -113,22 +113,22 @@ (-> Text (List [Text Definition]) (List [Name Type])) (|> definitions (list.filter (function (_ [name [def-type def-anns def-value]]) - (macro.struct? def-anns))) - (list;map (function (_ [name [def-type def-anns def-value]]) + (macro.structure? def-anns))) + (list@map (function (_ [name [def-type def-anns def-value]]) [[this-module-name name] def-type])))) (def: local-env (Meta (List [Name Type])) (do macro.monad [local-batches macro.locals - #let [total-locals (list;fold (function (_ [name type] table) - (dict.put~ name type table)) + #let [total-locals (list@fold (function (_ [name type] table) + (dict.try-put name type table)) (: (Dictionary Text Type) (dict.new text.hash)) - (list;join local-batches))]] + (list@join local-batches))]] (wrap (|> total-locals dict.entries - (list;map (function (_ [name type]) [["" name] type])))))) + (list@map (function (_ [name type]) [["" name] type])))))) (def: local-structs (Meta (List [Name Type])) @@ -147,7 +147,7 @@ [exports (macro.exports imp-mod)] (wrap (prepare-definitions imp-mod exports)))) imp-mods)] - (wrap (list;join export-batches)))) + (wrap (list@join export-batches)))) (def: (apply-function-type func arg) (-> Type Type (Check Type)) @@ -203,7 +203,7 @@ (do macro.monad [compiler macro.get-compiler] (case (|> alts - (list;map (function (_ [alt-name alt-type]) + (list@map (function (_ [alt-name alt-type]) (case (check.run context (do check.monad [[tvars alt-type] (concrete-type alt-type) @@ -217,7 +217,7 @@ (#.Right =deps) (list [alt-name =deps])))) - list;join) + list@join) #.Nil (macro.fail (format "No candidates for provisioning: " (%type dep))) @@ -252,7 +252,7 @@ [compiler macro.get-compiler context macro.type-context] (case (|> alts - (list;map (function (_ [alt-name alt-type]) + (list@map (function (_ [alt-name alt-type]) (case (check.run context (do check.monad [[tvars alt-type] (concrete-type alt-type) @@ -268,7 +268,7 @@ (#.Right =deps) (list [alt-name =deps])))) - list;join) + list@join) #.Nil (macro.fail (format "No alternatives for " (%type (type.function input-types output-type)))) @@ -303,7 +303,7 @@ (code.identifier constructor) _ - (` ((~ (code.identifier constructor)) (~+ (list;map instance$ dependencies)))))) + (` ((~ (code.identifier constructor)) (~+ (list@map instance$ dependencies)))))) (syntax: #export (::: {member s.identifier} @@ -346,19 +346,19 @@ (#.Cons chosen #.Nil) (wrap (list (` (:: (~ (instance$ chosen)) (~ (code.local-identifier (product.right member))) - (~+ (list;map code.identifier args)))))) + (~+ (list@map code.identifier args)))))) _ (macro.fail (format "Too many options available: " (|> chosen-ones - (list;map (|>> product.left %name)) + (list@map (|>> product.left %name)) (text.join-with ", ")) " --- for type: " (%type sig-type))))) (#.Right [args _]) (do @ [labels (|> (macro.gensym "") (list.repeat (list.size args)) (monad.seq @))] - (wrap (list (` (let [(~+ (|> (list.zip2 labels args) (list;map join-pair) list;join))] + (wrap (list (` (let [(~+ (|> (list.zip2 labels args) (list@map join-pair) list@join))] (..::: (~ (code.identifier member)) (~+ labels))))))) )) @@ -376,14 +376,14 @@ (do @ [g!implicit+ (implicit-bindings (list.size structures))] (wrap (list (` (let [(~+ (|> (list.zip2 g!implicit+ structures) - (list;map (function (_ [g!implicit structure]) + (list@map (function (_ [g!implicit structure]) (list g!implicit structure))) - list;join))] + list@join))] (~ body))))))) (syntax: #export (implicit: {structures ..implicits}) (do @ [g!implicit+ (implicit-bindings (list.size structures))] (wrap (|> (list.zip2 g!implicit+ structures) - (list;map (function (_ [g!implicit structure]) + (list@map (function (_ [g!implicit structure]) (` (def: (~ g!implicit) (~ structure))))))))) diff --git a/stdlib/source/lux/type/resource.lux b/stdlib/source/lux/type/resource.lux index 1c8d0be1d..6cc8cc3ec 100644 --- a/stdlib/source/lux/type/resource.lux +++ b/stdlib/source/lux/type/resource.lux @@ -4,21 +4,21 @@ ["p" parser] ["ex" exception (#+ exception:)] ["." monad (#+ Monad do) - [indexed (#+ IxMonad)]]] + [indexed (#+ IxMonad)]] + [concurrency + ["." promise (#+ Promise)]]] [data ["." identity (#+ Identity)] ["." maybe] ["." product] - ["." number] + [number + ["." nat]] [text format] [collection - ["dict" dictionary (#+ Dictionary)] ["." set] ["." row (#+ Row)] - ["." list ("#;." functor fold)]]] - [concurrency - ["." promise (#+ Promise)]] + ["." list ("#@." functor fold)]]] ["." macro ["s" syntax (#+ Syntax syntax:)]] [type @@ -130,7 +130,7 @@ (def: indices (Syntax (List Nat)) - (s.tuple (loop [seen (set.new number.hash)] + (s.tuple (loop [seen (set.new nat.hash)] (do p.monad [done? s.end?] (if done? @@ -155,7 +155,7 @@ (#.Cons head tail) (do macro.monad - [#let [max-idx (list;fold n/max head tail)] + [#let [max-idx (list@fold n/max head tail)] g!inputs (<| (monad.seq @) (list.repeat (inc max-idx)) (macro.gensym "input")) #let [g!outputs (|> (monad.fold maybe.monad (function (_ from to) @@ -166,8 +166,8 @@ swaps) maybe.assume row.to-list) - g!inputsT+ (list;map (|>> (~) ..CK (`)) g!inputs) - g!outputsT+ (list;map (|>> (~) ..CK (`)) g!outputs)]] + g!inputsT+ (list@map (|>> (~) ..CK (`)) g!inputs) + g!outputsT+ (list@map (|>> (~) ..CK (`)) g!outputs)]] (wrap (list (` (: (All [(~+ g!inputs) (~ g!context)] (Procedure (~! <m>) [(~+ g!inputsT+) (~ g!context)] diff --git a/stdlib/source/test/lux.lux b/stdlib/source/test/lux.lux index f50cdf48a..191a664ce 100644 --- a/stdlib/source/test/lux.lux +++ b/stdlib/source/test/lux.lux @@ -118,17 +118,13 @@ ["#." macro] ["#." math] ["#." time] + ["#." type] ["#." host ["#/." jvm]]] ## [control ## [concurrency ## ## [semaphore (#+)] ## ]] - ## [type ## (#+) - ## ## [check (#+)] - ## ## [implicit (#+)] ## TODO: FIX Specially troublesome... - ## ## [resource (#+)] - ## [dynamic (#+)]] ## [compiler ## [default ## ["_default/." syntax] @@ -376,6 +372,8 @@ /math.test) (<| (_.context "/time") /time.test) + (<| (_.context "/type") + /type.test) (<| (_.context "/host Host-platform interoperation") ($_ _.and /host.test @@ -384,5 +382,7 @@ )) (program: args - (io (_.run! (<| (_.times 100) - ..test)))) + (<| io + _.run! + (_.times 100) + ..test)) diff --git a/stdlib/source/test/lux/macro/poly/equivalence.lux b/stdlib/source/test/lux/macro/poly/equivalence.lux index 941eb881f..41ae1ecd0 100644 --- a/stdlib/source/test/lux/macro/poly/equivalence.lux +++ b/stdlib/source/test/lux/macro/poly/equivalence.lux @@ -1,9 +1,9 @@ (.module: [lux #* data/text/format - [control/monad (#+ do)] ["r" math/random (#+ Random)] ["_" test (#+ Test)] + [control ["." monad (#+ do)]] [control [equivalence (#+ Equivalence)]] [data diff --git a/stdlib/source/test/lux/type.lux b/stdlib/source/test/lux/type.lux index 7f5d76730..1fcc7e3e9 100644 --- a/stdlib/source/test/lux/type.lux +++ b/stdlib/source/test/lux/type.lux @@ -1,39 +1,42 @@ (.module: - [lux #* + [lux (#- type) + data/text/format + ["M" control/monad (#+ do)] + ["r" math/random (#+ Random)] + ["_" test (#+ Test)] [control - ["M" monad (#+ do Monad)] pipe] [data ["." maybe] - [text - format] [collection - ["." list]]] - [math - ["r" random]] - ["&" type]] - lux/test) - -## [Utils] -(def: #export gen-short + ["." list]]]] + {1 + ["." / ("#@." equivalence)]} + ["." / #_ + ["#." check] + ["#." dynamic] + ["#." implicit] + ["#." resource]]) + +(def: short (r.Random Text) (do r.monad [size (|> r.nat (:: @ map (n/% 10)))] (r.unicode size))) -(def: #export gen-name +(def: name (r.Random Name) - (r.and gen-short gen-short)) + (r.and ..short ..short)) -(def: #export gen-type +(def: #export type (r.Random Type) - (let [(^open "R;.") r.monad] - (r.rec (function (_ gen-type) - (let [pairG (r.and gen-type gen-type) + (let [(^open "R@.") r.monad] + (r.rec (function (_ recur) + (let [pairG (r.and recur recur) idG r.nat - quantifiedG (r.and (R;wrap (list)) gen-type)] + quantifiedG (r.and (R@wrap (list)) recur)] ($_ r.or - (r.and gen-short (R;wrap (list))) + (r.and ..short (R@wrap (list))) pairG pairG pairG @@ -43,136 +46,122 @@ quantifiedG quantifiedG pairG - (r.and gen-name gen-type) + (r.and ..name recur) )))))) -## [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 = +(def: #export test + Test + (<| (_.context (%name (name-of /._))) + ($_ _.and + (do r.monad + [sample ..type] + (_.test "Every type is equal to itself." + (:: /.equivalence = sample sample))) + (_.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)))) + (let [base (#.Named ["" "a"] (#.Product Bit Int)) + aliased (#.Named ["" "c"] + (#.Named ["" "b"] + base))] + ($_ _.and + (_.test "Can remove aliases from an already-named type." + (:: /.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 - [<struct-tests> (do-template [<desc> <ctor> <dtor> <unit>] - [(test (format "Can build and tear-down " <desc> " types.") + (/.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)))))) + (do r.monad + [size (|> r.nat (:: @ map (n/% 3))) + members (|> ..type + (r.filter (function (_ type) + (case type + (^or (#.Sum _) (#.Product _)) + #0 + + _ + #1))) + (list.repeat size) + (M.seq @)) + #let [(^open "/@.") /.equivalence + (^open "list@.") (list.equivalence /.equivalence)]] + (`` ($_ _.and + (~~ (do-template [<desc> <ctor> <dtor> <unit>] + [(_.test (format "Can build and tear-down " <desc> " types.") (let [flat (|> members <ctor> <dtor>)] - (or (L;= members flat) - (and (L;= (list) members) - (L;= (list <unit>) flat)))))] - - ["variant" &.variant &.flatten-variant Nothing] - ["tuple" &.tuple &.flatten-tuple Any] - )] - ($_ seq - <struct-tests> - ))))) - -(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 - [<quant-tests> (do-template [<desc> <ctor> <dtor>] - [(test (format "Can build and tear-down " <desc> " types.") - (let [[flat-size flat-body] (|> extra (<ctor> size) <dtor>)] - (and (n/= size flat-size) - (&;= extra flat-body))))] - - ["universally-quantified" &.univ-q &.flatten-univ-q] - ["existentially-quantified" &.ex-q &.flatten-ex-q] - )] - ($_ seq - <quant-tests> - ))))) - -(def: extraction - Test - (_.test "Can extract types." - (let [example (: (Maybe Nat) - #.Nonae)] - (type;= (type (List Nat)) - (:by-example [a] - {(Maybe a) example} - (List a)))))) + (or (list@= members flat) + (and (list@= (list) members) + (list@= (list <unit>) flat)))))] + + ["variant" /.variant /.flatten-variant Nothing] + ["tuple" /.tuple /.flatten-tuple Any] + )) + ))) + (do r.monad + [size (|> r.nat (:: @ map (n/% 3))) + members (M.seq @ (list.repeat size ..type)) + extra (|> ..type + (r.filter (function (_ type) + (case type + (^or (#.Function _) (#.Apply _)) + #0 + + _ + #1)))) + #let [(^open "/@.") /.equivalence + (^open "list@.") (list.equivalence /.equivalence)]] + ($_ _.and + (_.test "Can build and tear-down function types." + (let [[inputs output] (|> (/.function members extra) /.flatten-function)] + (and (list@= 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)))) + )) + (do r.monad + [size (|> r.nat (:: @ map (n/% 3))) + extra (|> ..type + (r.filter (function (_ type) + (case type + (^or (#.UnivQ _) (#.ExQ _)) + #0 + + _ + #1)))) + #let [(^open "/@.") /.equivalence]] + (`` ($_ _.and + (~~ (do-template [<desc> <ctor> <dtor>] + [(_.test (format "Can build and tear-down " <desc> " types.") + (let [[flat-size flat-body] (|> extra (<ctor> size) <dtor>)] + (and (n/= size flat-size) + (/@= extra flat-body))))] + + ["universally-quantified" /.univ-q /.flatten-univ-q] + ["existentially-quantified" /.ex-q /.flatten-ex-q] + )) + ))) + (_.test (%name (name-of /.:by-example)) + (let [example (: (Maybe Nat) + #.None)] + (/@= (.type (List Nat)) + (/.:by-example [a] + {(Maybe a) example} + (List a))))) + + /check.test + /dynamic.test + /implicit.test + /resource.test + ))) diff --git a/stdlib/source/test/lux/type/check.lux b/stdlib/source/test/lux/type/check.lux index 45f1ce821..d73b2783d 100644 --- a/stdlib/source/test/lux/type/check.lux +++ b/stdlib/source/test/lux/type/check.lux @@ -1,24 +1,54 @@ (.module: - [lux #* + [lux (#- type) + data/text/format + [control ["." monad (#+ do)]] + ["r" math/random (#+ Random)] + ["_" test (#+ Test)] [control - ["." monad (#+ do Monad)] [pipe (#+ case>)]] [data ["." product] ["." maybe] - ["." number] - ["." text ("#;." equivalence)] + ["." text ("#@." equivalence)] + [number + ["." nat]] [collection - ["." list ("#;." functor)] + ["." list ("#@." functor)] ["." set]]] - [math - ["r" random]] - ["." type ("#;." equivalence) - ["@" check]]] - lux/test - ["." //]) + ["." type ("#@." equivalence)]] + {1 + ["." /]}) + +## TODO: Remove the following 3 definitions ASAP. //.type already exists... +(def: short + (r.Random Text) + (r.unicode 10)) + +(def: name + (r.Random Name) + (r.and ..short ..short)) + +(def: type + (r.Random Type) + (let [(^open "R@.") r.monad] + (r.rec (function (_ recur) + (let [pairG (r.and recur recur) + idG r.nat + quantifiedG (r.and (R@wrap (list)) recur)] + ($_ r.or + (r.and ..short (R@wrap (list))) + pairG + pairG + pairG + idG + idG + idG + quantifiedG + quantifiedG + pairG + (r.and ..name recur) + )))))) -## [Utils] (def: (valid-type? type) (-> Type Bit) (case type @@ -40,198 +70,177 @@ #0)) (def: (type-checks? input) - (-> (@.Check []) Bit) - (case (@.run @.fresh-context 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-short - nameR (|> //.gen-short (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)) + (-> 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)] + [_ (/.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.and 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?)))))) - )) - )) +(def: #export test + Test + (<| (_.context (%name (name-of /._))) + ($_ _.and + (do r.monad + [sample (|> ..type (r.filter valid-type?))] + ($_ _.and + (_.test "Any is the super-type of everything." + (/.checks? Any sample)) + (_.test "Nothing is the sub-type of everything." + (/.checks? sample Nothing)) + )) + ($_ _.and + (_.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))))) + ) + (do r.monad + [meta ..type + data ..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)))))) + (do r.monad + [#let [gen-short (r.ascii 10)] + nameL gen-short + nameR (|> gen-short (r.filter (|>> (text@= nameL) not))) + paramL ..type + paramR (|> ..type (r.filter (|>> (/.checks? paramL) not)))] + ($_ _.and + (_.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))))) + )) + ($_ _.and + (_.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)))) + ) + (do r.monad + [num-connections (|> r.nat (:: @ map (n/% 100))) + boundT (|> ..type (r.filter (|>> (case> (#.Var _) #0 _ #1)))) + pick-pcg (r.and r.nat r.nat)] + ($_ _.and + (_.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 nat.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/source/test/lux/type/dynamic.lux b/stdlib/source/test/lux/type/dynamic.lux index 70e26f743..e2564627a 100644 --- a/stdlib/source/test/lux/type/dynamic.lux +++ b/stdlib/source/test/lux/type/dynamic.lux @@ -1,31 +1,32 @@ (.module: [lux #* - [control - [monad (#+ do)]] + data/text/format + ["r" math/random (#+ Random)] + ["_" test (#+ Test)] + [control ["." monad (#+ do)]] [data - ["." error]] - [math - ["r" random]] - [type - ["/" dynamic (#+ Dynamic :dynamic :check)]]] - lux/test) + ["." error]]] + {1 + ["." / (#+ Dynamic :dynamic :check)]}) -(context: "Dynamic typing." - (do @ - [expected r.nat - #let [value (:dynamic expected)]] - ($_ seq - (test "Can check dynamic values." - (case (:check Nat value) - (#error.Success actual) - (n/= expected actual) - - (#error.Failure error) - false)) - (test "Cannot confuse types." - (case (:check Text value) - (#error.Success actual) - false - - (#error.Failure error) - true))))) +(def: #export test + Test + (<| (_.context (%name (name-of /._))) + (do r.monad + [expected r.nat + #let [value (:dynamic expected)]] + ($_ _.and + (_.test "Can check dynamic values." + (case (:check Nat value) + (#error.Success actual) + (n/= expected actual) + + (#error.Failure error) + false)) + (_.test "Cannot confuse types." + (case (:check Text value) + (#error.Success actual) + false + + (#error.Failure error) + true)))))) diff --git a/stdlib/source/test/lux/type/implicit.lux b/stdlib/source/test/lux/type/implicit.lux index dffd9496c..5383c252f 100644 --- a/stdlib/source/test/lux/type/implicit.lux +++ b/stdlib/source/test/lux/type/implicit.lux @@ -1,40 +1,41 @@ (.module: [lux #* - [io] + data/text/format + ["r" math/random (#+ Random)] + ["_" test (#+ Test)] + [control ["." monad (#+ do)]] [control - [equivalence] - [functor] - [monad (#+ Monad do)]] + [equivalence (#+)] + [functor (#+)]] [data - ["." bit ("#;." equivalence)] - [number] - [collection [list]]] - [math - ["r" random]] - [type implicit]] - lux/test) + ["." bit ("#@." equivalence)] + [number + ["." nat]] + [collection + ["." list]]]] + {1 + ["." /]}) -(context: "Automatic structure selection" - (<| (times 100) - (do @ +(def: #export test + Test + (<| (_.context (%name (name-of /._))) + (do r.monad [x r.nat y r.nat] - ($_ seq - (test "Can automatically select first-order structures." - (let [(^open "list;.") (list.equivalence number.equivalence)] - (and (bit;= (:: number.equivalence = x y) - (::: = x y)) - (list;= (list.n/range 1 10) - (::: map inc (list.n/range 0 9))) - ))) - - (test "Can automatically select second-order structures." - (::: = - (list.n/range 1 10) - (list.n/range 1 10))) - - (test "Can automatically select third-order structures." - (let [lln (::: map (list.n/range 1) - (list.n/range 1 10))] - (::: = lln lln))) + ($_ _.and + (_.test "Can automatically select first-order structures." + (let [(^open "list@.") (list.equivalence nat.equivalence)] + (and (bit@= (:: nat.equivalence = x y) + (/.::: = x y)) + (list@= (list.n/range 1 10) + (/.::: map inc (list.n/range 0 9))) + ))) + (_.test "Can automatically select second-order structures." + (/.::: = + (list.n/range 1 10) + (list.n/range 1 10))) + (_.test "Can automatically select third-order structures." + (let [lln (/.::: map (list.n/range 1) + (list.n/range 1 10))] + (/.::: = lln lln))) )))) diff --git a/stdlib/source/test/lux/type/resource.lux b/stdlib/source/test/lux/type/resource.lux index b04321cc2..15d7cd137 100644 --- a/stdlib/source/test/lux/type/resource.lux +++ b/stdlib/source/test/lux/type/resource.lux @@ -1,48 +1,50 @@ (.module: [lux #* + data/text/format + ["r" math/random (#+ Random)] + ["_" test (#+ Test)] [control [monad [indexed (#+ do)]]] - [type - ["." resource (#+ Res)]] ["." io]] - lux/test) + {1 + ["." / (#+ Res)]}) -(context: "Sub-structural typing." - ($_ seq - (test "Can produce and consume keys in an ordered manner." - (<| (n/= (n/+ 123 456)) - io.run - resource.run-sync - (do resource.sync - [res|left (resource.ordered-sync 123) - res|right (resource.ordered-sync 456) - right (resource.read-sync res|right) - left (resource.read-sync res|left)] - (wrap (n/+ left right))))) - - (test "Can exchange commutative keys." - (<| (n/= (n/+ 123 456)) - io.run - resource.run-sync - (do resource.sync - [res|left (resource.commutative-sync 123) - res|right (resource.commutative-sync 456) - _ (resource.exchange-sync [1 0]) - left (resource.read-sync res|left) - right (resource.read-sync res|right)] - (wrap (n/+ left right))))) - - (test "Can group and un-group keys." - (<| (n/= (n/+ 123 456)) - io.run - resource.run-sync - (do resource.sync - [res|left (resource.commutative-sync 123) - res|right (resource.commutative-sync 456) - _ (resource.group-sync 2) - _ (resource.un-group-sync 2) - right (resource.read-sync res|right) - left (resource.read-sync res|left)] - (wrap (n/+ left right))))) - )) +(def: #export test + Test + (<| (_.context (%name (name-of /._))) + ($_ _.and + (_.test "Can produce and consume keys in an ordered manner." + (<| (n/= (n/+ 123 456)) + io.run + /.run-sync + (do /.sync + [res|left (/.ordered-sync 123) + res|right (/.ordered-sync 456) + right (/.read-sync res|right) + left (/.read-sync res|left)] + (wrap (n/+ left right))))) + (_.test "Can exchange commutative keys." + (<| (n/= (n/+ 123 456)) + io.run + /.run-sync + (do /.sync + [res|left (/.commutative-sync 123) + res|right (/.commutative-sync 456) + _ (/.exchange-sync [1 0]) + left (/.read-sync res|left) + right (/.read-sync res|right)] + (wrap (n/+ left right))))) + (_.test "Can group and un-group keys." + (<| (n/= (n/+ 123 456)) + io.run + /.run-sync + (do /.sync + [res|left (/.commutative-sync 123) + res|right (/.commutative-sync 456) + _ (/.group-sync 2) + _ (/.un-group-sync 2) + right (/.read-sync res|right) + left (/.read-sync res|left)] + (wrap (n/+ left right))))) + ))) |