aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux/type/implicit.lux44
-rw-r--r--stdlib/source/lux/type/resource.lux20
-rw-r--r--stdlib/source/test/lux.lux14
-rw-r--r--stdlib/source/test/lux/macro/poly/equivalence.lux2
-rw-r--r--stdlib/source/test/lux/type.lux287
-rw-r--r--stdlib/source/test/lux/type/check.lux395
-rw-r--r--stdlib/source/test/lux/type/dynamic.lux55
-rw-r--r--stdlib/source/test/lux/type/implicit.lux65
-rw-r--r--stdlib/source/test/lux/type/resource.lux84
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)))))
+ )))