aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/test')
-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
7 files changed, 452 insertions, 450 deletions
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)))))
+ )))
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 14:22:29 +0000