- Updated tests for lux/type.

- Added tests for lux/type/check and lux/type/auto.

4 files changed, 328 insertions, 42 deletions

diff --git a/stdlib/test/test/lux/type.lux b/stdlib/test/test/lux/type.lux
index 8fa871e70..0e203f376 100644
--- a/stdlib/test/test/lux/type.lux
+++ b/stdlib/test/test/lux/type.lux
@@ -1,41 +1,137 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
 (;module:
   lux
   (lux (codata [io])
        (control monad)
        (data [text "Text/" Monoid<Text>]
-             [number])
-       type
-       (codata function))
+             text/format
+             [number]
+             maybe
+             (struct [list]))
+       (math ["R" random])
+       pipe
+       ["&" type])
   lux/test)
 
-(test: "lux/type exports"
-  (let% [<eq-tests> (do-template [<type>]
-                      [(match true (:: Eq<Type> = <type> <type>))]
-
-                      [(#;HostT "java.util.List" (list Int))]
-                      [#;UnitT]
-                      [#;VoidT]
-                      [(#;VarT +123)]
-                      [(#;ExT +123)]
-                      [(#;BoundT +123)]
-                      [(#;LambdaT Bool Int)]
-                      [(#;AppT List Int)]
-                      [(#;NamedT ["" "Int-List"] (#;AppT List Int))]
-                      [(#;SumT Bool Int)]
-                      [(#;ProdT Bool Int)]
-                      [(#;UnivQ (list) (#;ProdT Bool (#;BoundT +1)))]
-                      [(#;ExQ (list) (#;ProdT Bool (#;BoundT +1)))]
-                      )]
-    (test-all <eq-tests>
-              (match (^=> (#;Some _type) (:: Eq<Type> = _type (#;ProdT Bool Int)))
-                     (apply-type (type (Meta Bool)) Int))
-              (match #;None (apply-type Text Bool))
-              (match true
-                     (:: Eq<Type> =
-                         (#;NamedT ["" "a"]
-                                   (#;ProdT Bool Int))
-                         (un-alias (#;NamedT ["" "c"]
-                                             (#;NamedT ["" "b"]
-                                                       (#;NamedT ["" "a"]
-                                                                 (#;ProdT Bool Int)))))))
-              )))
+## [Utils]
+(def: gen-name
+  (R;Random Text)
+  (do R;Monad<Random>
+    [size (|> R;nat (:: @ map (n.% +10)))]
+    (R;text size)))
+
+(def: gen-ident
+  (R;Random Ident)
+  (R;seq gen-name gen-name))
+
+(def: gen-type
+  (R;Random Type)
+  (let [(^open "R/") R;Monad<Random>]
+    (R;rec (lambda [gen-type]
+             ($_ R;alt
+                 (R;seq gen-name (R/wrap (list)))
+                 (R/wrap [])
+                 (R/wrap [])
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 R;nat
+                 R;nat
+                 R;nat
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-ident gen-type)
+                 )))))
+
+## [Tests]
+(test: "Types"
+  [sample gen-type]
+  (assert "Every type is equal to itself."
+          (:: &;Eq<Type> = sample sample)))
+
+(test: "Type application"
+  (assert "Can apply quantified types (universal and existential quantification)."
+          (and (default false
+                 (do Monad<Maybe>
+                   [partial (&;apply-type Meta Bool)
+                    full (&;apply-type partial Int)]
+                   (wrap (:: &;Eq<Type> = full (#;ProdT Bool Int)))))
+               (|> (&;apply-type Text Bool)
+                   (case> #;None true _ false)))))
+
+(test: "Naming"
+  (let [base (#;NamedT ["" "a"] (#;ProdT Bool Int))
+        aliased (#;NamedT ["" "c"]
+                          (#;NamedT ["" "b"]
+                                    base))]
+    ($_ seq
+        (assert "Can remove aliases from an already-named type."
+                (:: &;Eq<Type> =
+                    base
+                    (&;un-alias aliased)))
+
+        (assert "Can remove all names from a type."
+                (and (not (:: &;Eq<Type> =
+                              base
+                              (&;un-name aliased)))
+                     (:: &;Eq<Type> =
+                         (&;un-name base)
+                         (&;un-name aliased)))))))
+
+(test: "Type construction [structs]"
+  [size (|> R;nat (:: @ map (n.% +3)))
+   members (seqM @ (list;repeat size gen-type))
+   #let [(^open "&/") &;Eq<Type>
+         (^open "L/") (list;Eq<List> &;Eq<Type>)]]
+  (let% [<struct-tests> (do-template [<desc> <ctor> <dtor> <unit>]
+                          [(assert (format "Can build and tear-down " <desc> " types.")
+                                   (let [flat (|> members <ctor> <dtor>)]
+                                     (or (n.= (list;size members) (list;size flat))
+                                         (and (n.= +0 (list;size members))
+                                              (n.= +1 (list;size flat))
+                                              (|> flat list;head (default (undefined)) (&/= <unit>))))))]
+
+                          ["variant" &;variant &;flatten-variant #;VoidT]
+                          ["tuple"   &;tuple   &;flatten-tuple   #;UnitT]
+                          )]
+    ($_ seq
+        <struct-tests>
+        )))
+
+(test: "Type construction [parameterized]"
+  [size (|> R;nat (:: @ map (n.% +3)))
+   members (seqM @ (list;repeat size gen-type))
+   extra gen-type
+   #let [(^open "&/") &;Eq<Type>
+         (^open "L/") (list;Eq<List> &;Eq<Type>)]]
+  ($_ seq
+      (assert "Can build and tear-down function types."
+              (let [[inputs output] (|> (&;function members extra) &;flatten-function)]
+                (n.= (list;size members) (list;size inputs))))
+
+      (assert "Can build and tear-down application types."
+              (let [[tfunc tparams] (|> members (&;application extra) &;flatten-application)]
+                (n.= (list;size members) (list;size tparams))))
+      ))
+
+(test: "Type construction [higher order]"
+  [size (|> R;nat (:: @ map (n.% +3)))
+   extra gen-type
+   #let [(^open "&/") &;Eq<Type>]]
+  (let% [<quant-tests> (do-template [<desc> <ctor> <dtor>]
+                         [(assert (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"   &;univq &;flatten-univq]
+                         ["existentially-quantified" &;exq   &;flatten-exq]
+                         )]
+    ($_ seq
+        <quant-tests>
+        )))
diff --git a/stdlib/test/test/lux/type/auto.lux b/stdlib/test/test/lux/type/auto.lux
new file mode 100644
index 000000000..ef69961cd
--- /dev/null
+++ b/stdlib/test/test/lux/type/auto.lux
@@ -0,0 +1,28 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(;module:
+  lux
+  (lux (codata [io])
+       (control monad
+                [eq])
+       (data [text "Text/" Monoid<Text>]
+             text/format
+             [number]
+             [bool "B/" Eq<Bool>]
+             maybe
+             (struct [list]))
+       (math ["R" random])
+       pipe
+       [type]
+       type/auto)
+  lux/test)
+
+(test: "Automatic structure selection"
+  [x R;nat
+   y R;nat]
+  (assert "Can automatically select first-order structures."
+          (B/= (:: number;Eq<Nat> = x y)
+               (::: eq;= x y))))
diff --git a/stdlib/test/test/lux/type/check.lux b/stdlib/test/test/lux/type/check.lux
new file mode 100644
index 000000000..273dbad4c
--- /dev/null
+++ b/stdlib/test/test/lux/type/check.lux
@@ -0,0 +1,162 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(;module:
+  lux
+  (lux (codata [io])
+       (control monad)
+       (data [text "Text/" Monoid<Text>]
+             text/format
+             [number]
+             maybe
+             (struct [list]))
+       (math ["R" random])
+       pipe
+       [type]
+       ["&" type/check])
+  lux/test)
+
+## [Utils]
+(def: gen-name
+  (R;Random Text)
+  (do R;Monad<Random>
+    [size (|> R;nat (:: @ map (n.% +10)))]
+    (R;text size)))
+
+(def: gen-ident
+  (R;Random Ident)
+  (R;seq gen-name gen-name))
+
+(def: gen-type
+  (R;Random Type)
+  (let [(^open "R/") R;Monad<Random>]
+    (R;rec (lambda [gen-type]
+             ($_ R;alt
+                 (R;seq gen-name (R/wrap (list)))
+                 (R/wrap [])
+                 (R/wrap [])
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-type gen-type)
+                 R;nat
+                 R;nat
+                 R;nat
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq (R/wrap (list)) gen-type)
+                 (R;seq gen-type gen-type)
+                 (R;seq gen-ident gen-type)
+                 )))))
+
+(def: (type-checks? input)
+  (-> (&;Check []) Bool)
+  (case (&;run &;fresh-context input)
+    (#;Right [])
+    true
+
+    (#;Left error)
+    false))
+
+## [Tests]
+(test: "Top and Bottom"
+  [sample gen-type]
+  ($_ seq
+      (assert "Top is the super-type 0f everything."
+              (&;checks? Top sample))
+
+      (assert "Bottom is the sub-type 0f everything."
+              (&;checks? sample Bottom))
+      ))
+
+(test: "Simple type-checking."
+  ($_ seq
+      (assert "Unit and Void match themselves."
+              (and (&;checks? Void Void)
+                   (&;checks? Unit Unit)))
+
+      (assert "Existential types only match with themselves."
+              (and (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check ex ex)))
+                   (not (type-checks? (do &;Monad<Check>
+                                        [[lid lex] &;existential
+                                         [rid rex] &;existential]
+                                        (&;check lex rex))))))
+
+      (assert "Names don't affect type-checking."
+              (and (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check (#;NamedT ["module" "name"] ex)
+                                            ex)))
+                   (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check ex
+                                            (#;NamedT ["module" "name"] ex))))
+                   (type-checks? (do &;Monad<Check>
+                                   [[id ex] &;existential]
+                                   (&;check (#;NamedT ["module" "name"] ex)
+                                            (#;NamedT ["module" "name"] ex))))))
+
+      (assert "Can type-check functions."
+              (and (&;checks? (#;LambdaT Bottom Top)
+                              (#;LambdaT Top Bottom))
+                   (not (&;checks? (#;LambdaT Top Bottom)
+                                   (#;LambdaT Bottom Top)))))
+      ))
+
+(test: "Type application"
+  [meta gen-type
+   data gen-type]
+  (assert "Can type-check type application."
+          (and (&;checks? (#;AppT (#;AppT Meta meta) data)
+                          (type;tuple (list meta data)))
+               (&;checks? (type;tuple (list meta data))
+                          (#;AppT (#;AppT Meta meta) data)))))
+
+(test: "Host types"
+  [nameL gen-name
+   nameR gen-name
+   paramL gen-type
+   paramR gen-type]
+  ($_ seq
+      (assert "Host types match when they have the same name and the same parameters."
+              (&;checks? (#;HostT nameL (list paramL))
+                         (#;HostT nameL (list paramL))))
+
+      (assert "Names matter to host types."
+              (&;checks? (#;HostT nameL (list paramL))
+                         (#;HostT nameR (list paramL))))
+
+      (assert "Parameters matter to host types."
+              (&;checks? (#;HostT nameL (list paramL))
+                         (#;HostT nameL (list paramR))))
+      ))
+
+(test: "Type-vars"
+  ($_ seq
+      (assert "Type-vars check against themselves."
+              (type-checks? (&;with-var (lambda [[id var]] (&;check var var)))))
+
+      (assert "Can bind unbound type-vars by type-checking against them."
+              (and (type-checks? (&;with-var (lambda [[id var]] (&;check var #;UnitT))))
+                   (type-checks? (&;with-var (lambda [[id var]] (&;check #;UnitT var))))))
+
+      (assert "Can't rebind already bound type-vars."
+              (not (type-checks? (&;with-var (lambda [[id var]]
+                                               (do &;Monad<Check>
+                                                 [_ (&;check var #;UnitT)]
+                                                 (&;check var #;VoidT)))))))
+
+      (assert "If the type bound to a var is a super-type to another, then the var is also a super-type."
+              (type-checks? (&;with-var (lambda [[id var]]
+                                          (do &;Monad<Check>
+                                            [_ (&;check var Top)]
+                                            (&;check var #;UnitT))))))
+
+      (assert "If the type bound to a var is a sub-type of another, then the var is also a sub-type."
+              (type-checks? (&;with-var (lambda [[id var]]
+                                          (do &;Monad<Check>
+                                            [_ (&;check var Bottom)]
+                                            (&;check #;UnitT var))))))
+      ))
diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux
index e225e1f28..ef94dca90 100644
--- a/stdlib/test/tests.lux
+++ b/stdlib/test/tests.lux
@@ -59,17 +59,17 @@
              (macro ["_;" ast]
                     ["_;" syntax]
                     ["_;" template])
-             ## [type]
-             ## (type [check] [auto])
-             ## (control ...)
+             ["_;" type]
+             (type ["_;" check]
+                   ["_;" auto])
+             ## (control [effect])
              )
         )
   ## (lux (codata [cont])
-  ## (macro [poly]
-  ##        (poly ["poly_;" eq]
-  ##              ["poly_;" text-encoder]
-  ##              ["poly_;" functor]))
-  ##      (control [effect]))
+  ##      (macro [poly]
+  ##             (poly ["poly_;" eq]
+  ##                   ["poly_;" text-encoder]
+  ##                   ["poly_;" functor])))
   )
 
 ## [Program]