From a8d76e48df01d0f5326faa8456797f91cb2cbeba Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 30 Jun 2022 22:53:23 -0400 Subject: Alternative names for (un)quoting macros. --- stdlib/source/test/lux.lux | 2 - stdlib/source/test/lux/control/concurrency/frp.lux | 5 +- .../test/lux/control/concurrency/semaphore.lux | 5 +- stdlib/source/test/lux/control/region.lux | 5 +- stdlib/source/test/lux/data/binary.lux | 4 +- .../test/lux/data/collection/tree/finger.lux | 3 +- stdlib/source/test/lux/data/format/json.lux | 6 +- stdlib/source/test/lux/data/format/xml.lux | 4 +- stdlib/source/test/lux/data/text.lux | 8 +- stdlib/source/test/lux/debug.lux | 4 +- stdlib/source/test/lux/ffi.jvm.lux | 4 +- stdlib/source/test/lux/math/modular.lux | 5 +- stdlib/source/test/lux/meta.lux | 8 +- stdlib/source/test/lux/meta/type.lux | 567 +++++++++++++ stdlib/source/test/lux/meta/type/check.lux | 900 +++++++++++++++++++++ stdlib/source/test/lux/meta/type/dynamic.lux | 48 ++ stdlib/source/test/lux/meta/type/implicit.lux | 64 ++ stdlib/source/test/lux/meta/type/primitive.lux | 89 ++ stdlib/source/test/lux/meta/type/quotient.lux | 60 ++ stdlib/source/test/lux/meta/type/refinement.lux | 91 +++ stdlib/source/test/lux/meta/type/resource.lux | 191 +++++ stdlib/source/test/lux/meta/type/unit.lux | 118 +++ stdlib/source/test/lux/meta/type/unit/scale.lux | 97 +++ stdlib/source/test/lux/meta/type/variance.lux | 35 + .../compiler/language/lux/analysis/inference.lux | 6 +- .../tool/compiler/language/lux/analysis/scope.lux | 5 +- .../tool/compiler/language/lux/analysis/type.lux | 6 +- .../tool/compiler/language/lux/phase/analysis.lux | 5 +- .../compiler/language/lux/phase/analysis/case.lux | 5 +- .../language/lux/phase/analysis/complex.lux | 6 +- .../language/lux/phase/analysis/function.lux | 8 +- .../language/lux/phase/analysis/reference.lux | 5 +- .../language/lux/phase/analysis/simple.lux | 6 +- .../language/lux/phase/extension/analysis/lux.lux | 4 +- stdlib/source/test/lux/type.lux | 567 ------------- stdlib/source/test/lux/type/check.lux | 900 --------------------- stdlib/source/test/lux/type/dynamic.lux | 48 -- stdlib/source/test/lux/type/implicit.lux | 64 -- stdlib/source/test/lux/type/primitive.lux | 89 -- stdlib/source/test/lux/type/quotient.lux | 60 -- stdlib/source/test/lux/type/refinement.lux | 91 --- stdlib/source/test/lux/type/resource.lux | 191 ----- stdlib/source/test/lux/type/unit.lux | 118 --- stdlib/source/test/lux/type/unit/scale.lux | 97 --- stdlib/source/test/lux/type/variance.lux | 35 - stdlib/source/test/lux/world/file/watch.lux | 4 +- 46 files changed, 2326 insertions(+), 2317 deletions(-) create mode 100644 stdlib/source/test/lux/meta/type.lux create mode 100644 stdlib/source/test/lux/meta/type/check.lux create mode 100644 stdlib/source/test/lux/meta/type/dynamic.lux create mode 100644 stdlib/source/test/lux/meta/type/implicit.lux create mode 100644 stdlib/source/test/lux/meta/type/primitive.lux create mode 100644 stdlib/source/test/lux/meta/type/quotient.lux create mode 100644 stdlib/source/test/lux/meta/type/refinement.lux create mode 100644 stdlib/source/test/lux/meta/type/resource.lux create mode 100644 stdlib/source/test/lux/meta/type/unit.lux create mode 100644 stdlib/source/test/lux/meta/type/unit/scale.lux create mode 100644 stdlib/source/test/lux/meta/type/variance.lux delete mode 100644 stdlib/source/test/lux/type.lux delete mode 100644 stdlib/source/test/lux/type/check.lux delete mode 100644 stdlib/source/test/lux/type/dynamic.lux delete mode 100644 stdlib/source/test/lux/type/implicit.lux delete mode 100644 stdlib/source/test/lux/type/primitive.lux delete mode 100644 stdlib/source/test/lux/type/quotient.lux delete mode 100644 stdlib/source/test/lux/type/refinement.lux delete mode 100644 stdlib/source/test/lux/type/resource.lux delete mode 100644 stdlib/source/test/lux/type/unit.lux delete mode 100644 stdlib/source/test/lux/type/unit/scale.lux delete mode 100644 stdlib/source/test/lux/type/variance.lux (limited to 'stdlib/source/test') diff --git a/stdlib/source/test/lux.lux b/stdlib/source/test/lux.lux index af6864ce3..04f893c8f 100644 --- a/stdlib/source/test/lux.lux +++ b/stdlib/source/test/lux.lux @@ -58,7 +58,6 @@ ["[1][0]" time] ["[1][0]" tool] - ["[1][0]" type] ["[1][0]" world] ["[1][0]" ffi] @@ -1224,7 +1223,6 @@ /time.test /tool.test - /type.test /world.test /ffi.test diff --git a/stdlib/source/test/lux/control/concurrency/frp.lux b/stdlib/source/test/lux/control/concurrency/frp.lux index 232e483d7..8a279bac2 100644 --- a/stdlib/source/test/lux/control/concurrency/frp.lux +++ b/stdlib/source/test/lux/control/concurrency/frp.lux @@ -20,8 +20,9 @@ ["[0]" random] [number ["n" nat]]] - [type - ["[0]" variance]]]] + [meta + [type + ["[0]" variance]]]]] [\\library ["[0]" / (.only) [// diff --git a/stdlib/source/test/lux/control/concurrency/semaphore.lux b/stdlib/source/test/lux/control/concurrency/semaphore.lux index eeaac1f53..4bae6dd3f 100644 --- a/stdlib/source/test/lux/control/concurrency/semaphore.lux +++ b/stdlib/source/test/lux/control/concurrency/semaphore.lux @@ -24,8 +24,9 @@ [number ["n" nat] ["[0]" i64]]] - [type - ["[0]" refinement]]]] + [meta + [type + ["[0]" refinement]]]]] [\\library ["[0]" /]]) diff --git a/stdlib/source/test/lux/control/region.lux b/stdlib/source/test/lux/control/region.lux index 54dde9289..e0ef106a2 100644 --- a/stdlib/source/test/lux/control/region.lux +++ b/stdlib/source/test/lux/control/region.lux @@ -1,7 +1,6 @@ (.require [library [lux (.except) - [type (.only sharing)] ["_" test (.only Test)] [abstract [equivalence (.only Equivalence)] @@ -21,7 +20,9 @@ [math ["[0]" random] [number - ["n" nat]]]]] + ["n" nat]]] + [meta + [type (.only sharing)]]]] [\\library ["[0]" / (.only Region) [// diff --git a/stdlib/source/test/lux/data/binary.lux b/stdlib/source/test/lux/data/binary.lux index 52fa6519a..5bd685351 100644 --- a/stdlib/source/test/lux/data/binary.lux +++ b/stdlib/source/test/lux/data/binary.lux @@ -3,7 +3,6 @@ [lux (.except) [ffi (.only)] ["_" test (.only Test)] - ["[0]" type] [abstract [equivalence (.only Equivalence)] ["[0]" monad (.only do)] @@ -44,7 +43,8 @@ ["[0]" rev] ["[0]" frac]]] [meta - ["[0]" symbol]]]] + ["[0]" symbol] + ["[0]" type]]]] [\\library ["[0]" / (.only) (.use "[1]#[0]" equivalence) ["!" \\unsafe] diff --git a/stdlib/source/test/lux/data/collection/tree/finger.lux b/stdlib/source/test/lux/data/collection/tree/finger.lux index 2f9e4c374..7d9faf595 100644 --- a/stdlib/source/test/lux/data/collection/tree/finger.lux +++ b/stdlib/source/test/lux/data/collection/tree/finger.lux @@ -14,7 +14,8 @@ ["[0]" random] [number ["n" nat]]] - [type (.only by_example)]]] + [meta + [type (.only by_example)]]]] [\\library ["[0]" /]]) diff --git a/stdlib/source/test/lux/data/format/json.lux b/stdlib/source/test/lux/data/format/json.lux index 7be586b4f..75d616037 100644 --- a/stdlib/source/test/lux/data/format/json.lux +++ b/stdlib/source/test/lux/data/format/json.lux @@ -3,7 +3,6 @@ [lux (.except Variant Record) ["_" test (.only Test)] ["@" target] - ["[0]" meta] [abstract [codec (.except)] [monad (.only do)] @@ -43,8 +42,9 @@ ["[0]/[1]" \\test]] ["[0]" duration ["[0]/[1]" \\test]]] - [type - ["[0]" unit]]]] + ["[0]" meta (.only) + [type + ["[0]" unit]]]]] ["[0]" \\polytypic] ["[0]" \\parser] [\\library diff --git a/stdlib/source/test/lux/data/format/xml.lux b/stdlib/source/test/lux/data/format/xml.lux index 53f9346c0..a01fab3e8 100644 --- a/stdlib/source/test/lux/data/format/xml.lux +++ b/stdlib/source/test/lux/data/format/xml.lux @@ -2,7 +2,6 @@ [library [lux (.except char symbol) ["_" test (.only Test)] - ["[0]" type (.use "[1]#[0]" equivalence)] [abstract [monad (.only do)] [\\specification @@ -27,7 +26,8 @@ [number ["n" nat]]] [meta - ["[0]" symbol (.use "[1]#[0]" equivalence)]]]] + ["[0]" symbol (.use "[1]#[0]" equivalence)] + ["[0]" type (.use "[1]#[0]" equivalence)]]]] ["[0]" \\parser] [\\library ["[0]" / (.use "[1]#[0]" equivalence)]]) diff --git a/stdlib/source/test/lux/data/text.lux b/stdlib/source/test/lux/data/text.lux index 0f7e49f03..ca4866bc4 100644 --- a/stdlib/source/test/lux/data/text.lux +++ b/stdlib/source/test/lux/data/text.lux @@ -2,7 +2,6 @@ [library [lux (.except char) ["_" test (.only Test)] - ["[0]" type] [abstract [monad (.only do)] [equivalence (.only Equivalence)] @@ -50,7 +49,8 @@ ["[0]" ratio]]] [meta ["[0]" location] - ["[0]" symbol]] + ["[0]" symbol] + ["[0]" type]] ["[0]" time (.only) ["[0]" day] ["[0]" month] @@ -62,11 +62,11 @@ ["[1][0]" xml] ["[1][0]" json]] [// - ["[1][0]" type] [macro ["[1][0]" code]] [meta - ["[1][0]" symbol]]]] + ["[1][0]" symbol] + ["[1][0]" type]]]] ["[0]" / ["[1][0]" buffer] ["[1][0]" encoding] diff --git a/stdlib/source/test/lux/debug.lux b/stdlib/source/test/lux/debug.lux index 978f42916..d85343bc9 100644 --- a/stdlib/source/test/lux/debug.lux +++ b/stdlib/source/test/lux/debug.lux @@ -33,7 +33,6 @@ [\\library ["[0]" /]] ["$[0]" // - ["[1][0]" type] [data [format ["[1][0]" json] @@ -45,7 +44,8 @@ ["[1][0]" ratio]]] [meta ["[1][0]" location] - ["[1][0]" symbol]]]) + ["[1][0]" symbol] + ["[1][0]" type]]]) (def can_represent_simple_types (Random Bit) diff --git a/stdlib/source/test/lux/ffi.jvm.lux b/stdlib/source/test/lux/ffi.jvm.lux index 581d89f2d..13c9f2fcd 100644 --- a/stdlib/source/test/lux/ffi.jvm.lux +++ b/stdlib/source/test/lux/ffi.jvm.lux @@ -2,8 +2,6 @@ [library [lux (.except) ["_" test (.only Test)] - ["[0]" type (.use "[1]#[0]" equivalence)] - ["[0]" meta] ["[0]" debug] ["[0]" static] [abstract @@ -31,6 +29,8 @@ ["n" nat] ["i" int (.use "[1]#[0]" equivalence)] ["f" frac (.use "[1]#[0]" equivalence)]]] + ["[0]" meta (.only) + ["[0]" type (.use "[1]#[0]" equivalence)]] [target ["[0]" jvm ["[1]" type (.use "[1]#[0]" equivalence)]]]]] diff --git a/stdlib/source/test/lux/math/modular.lux b/stdlib/source/test/lux/math/modular.lux index c3a1b8f53..60734f83d 100644 --- a/stdlib/source/test/lux/math/modular.lux +++ b/stdlib/source/test/lux/math/modular.lux @@ -2,7 +2,6 @@ [library [lux (.except) ["_" test (.only Test)] - ["[0]" type (.use "[1]#[0]" equivalence)] [abstract [monad (.only do)] [\\specification @@ -21,7 +20,9 @@ [math ["[0]" random (.only Random)] [number - ["i" int]]]]] + ["i" int]]] + [meta + ["[0]" type (.use "[1]#[0]" equivalence)]]]] ["$[0]" // ["[1]" modulus]] [\\library diff --git a/stdlib/source/test/lux/meta.lux b/stdlib/source/test/lux/meta.lux index 51b89ebfc..e5166d7ee 100644 --- a/stdlib/source/test/lux/meta.lux +++ b/stdlib/source/test/lux/meta.lux @@ -2,7 +2,6 @@ [library [lux (.except) ["_" test (.only Test)] - ["[0]" type (.use "[1]#[0]" equivalence)] [abstract [equivalence (.only Equivalence)] [monad (.only do)] @@ -31,12 +30,14 @@ ["[0]" location] ["[0]" symbol (.use "[1]#[0]" equivalence)]]]] [\\library - ["[0]" /]] + ["[0]" / (.only) + ["[0]" type (.use "[1]#[0]" equivalence)]]] ["[0]" / ["[1][0]" location] ["[1][0]" symbol] ["[1][0]" configuration] - ["[1][0]" version]]) + ["[1][0]" version] + ["[1][0]" type]]) (def !expect (template (_ ) @@ -1020,4 +1021,5 @@ /symbol.test /configuration.test /version.test + /type.test ))) diff --git a/stdlib/source/test/lux/meta/type.lux b/stdlib/source/test/lux/meta/type.lux new file mode 100644 index 000000000..9f753b1d0 --- /dev/null +++ b/stdlib/source/test/lux/meta/type.lux @@ -0,0 +1,567 @@ +(.require + [library + [lux (.except symbol) + ["_" test (.only Test)] + [abstract + ["[0]" monad (.only do)] + [\\specification + ["$[0]" equivalence]]] + [control + ["<>" parser] + ["[0]" pipe] + ["[0]" maybe] + ["[0]" try] + ["[0]" exception]] + [data + ["[0]" bit (.use "[1]#[0]" equivalence)] + ["[0]" text (.use "[1]#[0]" equivalence) + ["%" \\format (.only format)]] + [collection + ["[0]" list] + ["[0]" array]]] + [macro + ["^" pattern] + ["[0]" code (.use "[1]#[0]" equivalence)]] + [math + ["[0]" random (.only Random) (.use "[1]#[0]" monad)] + [number + ["n" nat]]] + [meta + ["[0]" symbol (.use "[1]#[0]" equivalence)]]]] + ["[0]" \\parser] + [\\library + ["[0]" / (.use "[1]#[0]" equivalence)]] + ["[0]" / + ["[1][0]" primitive] + ["[1][0]" check] + ["[1][0]" dynamic] + ["[1][0]" implicit] + ["[1][0]" quotient] + ["[1][0]" refinement] + ["[1][0]" resource] + ["[1][0]" unit] + ["[1][0]" variance]]) + +(def !expect + (template (_ ) + [(case + + true + + _ + false)])) + +(def primitive + (Random Type) + (|> (random.alpha_numeric 1) + (at random.monad each (function (_ name) + {.#Primitive name (list)})))) + +(def test|matches + Test + (<| (_.for [\\parser.types_do_not_match]) + (do [! random.monad] + [expected ..primitive + dummy (random.only (|>> (/#= expected) not) + ..primitive)]) + (all _.and + (_.coverage [\\parser.exactly] + (and (|> (\\parser.result (\\parser.exactly expected) expected) + (!expect {try.#Success []})) + (|> (\\parser.result (\\parser.exactly expected) dummy) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.types_do_not_match error)))))) + (_.coverage [\\parser.sub] + (and (|> (\\parser.result (\\parser.sub expected) expected) + (!expect {try.#Success []})) + (|> (\\parser.result (\\parser.sub Any) expected) + (!expect {try.#Success []})) + (|> (\\parser.result (\\parser.sub expected) Nothing) + (!expect {try.#Success []})) + (|> (\\parser.result (\\parser.sub expected) dummy) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.types_do_not_match error)))))) + (_.coverage [\\parser.super] + (and (|> (\\parser.result (\\parser.super expected) expected) + (!expect {try.#Success []})) + (|> (\\parser.result (\\parser.super expected) Any) + (!expect {try.#Success []})) + (|> (\\parser.result (\\parser.super Nothing) expected) + (!expect {try.#Success []})) + (|> (\\parser.result (\\parser.super expected) dummy) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.types_do_not_match error)))))) + ))) + +(def test|aggregate + Test + (do [! random.monad] + [expected_left ..primitive + expected_middle ..primitive + expected_right ..primitive] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage [ ] + (and (|> (\\parser.result ( (all <>.and \\parser.any \\parser.any \\parser.any)) + ( (list expected_left expected_middle expected_right))) + (!expect (^.multi {try.#Success [actual_left actual_middle actual_right]} + (and (/#= expected_left actual_left) + (/#= expected_middle actual_middle) + (/#= expected_right actual_right))))) + (|> (\\parser.result ( (all <>.and \\parser.any \\parser.any \\parser.any)) + ( (list expected_left expected_middle expected_right))) + (!expect (^.multi {try.#Failure error} + (exception.match? error))))))] + + [\\parser.variant \\parser.not_variant /.variant /.tuple] + [\\parser.tuple \\parser.not_tuple /.tuple /.variant] + )) + + (_.coverage [\\parser.function \\parser.not_function] + (and (|> (\\parser.result (\\parser.function (all <>.and \\parser.any \\parser.any) \\parser.any) + (/.function (list expected_left expected_middle) expected_right)) + (!expect (^.multi {try.#Success [[actual_left actual_middle] actual_right]} + (and (/#= expected_left actual_left) + (/#= expected_middle actual_middle) + (/#= expected_right actual_right))))) + (|> (\\parser.result (\\parser.function (all <>.and \\parser.any \\parser.any) \\parser.any) + (/.variant (list expected_left expected_middle expected_right))) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.not_function error)))))) + (_.coverage [\\parser.applied \\parser.not_application] + (and (|> (\\parser.result (\\parser.applied (all <>.and \\parser.any \\parser.any \\parser.any)) + (/.application (list expected_middle expected_right) expected_left)) + (!expect (^.multi {try.#Success [actual_left actual_middle actual_right]} + (and (/#= expected_left actual_left) + (/#= expected_middle actual_middle) + (/#= expected_right actual_right))))) + (|> (\\parser.result (\\parser.applied (all <>.and \\parser.any \\parser.any \\parser.any)) + (/.variant (list expected_left expected_middle expected_right))) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.not_application error)))))) + )))) + +(def test|parameter + Test + (do random.monad + [quantification ..primitive + argument ..primitive + not_parameter ..primitive + parameter random.nat] + (all _.and + (_.coverage [\\parser.not_parameter] + (|> (\\parser.result \\parser.parameter not_parameter) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.not_parameter error))))) + (_.coverage [\\parser.unknown_parameter] + (|> (\\parser.result \\parser.parameter {.#Parameter parameter}) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.unknown_parameter error))))) + (_.coverage [\\parser.with_extension] + (|> (\\parser.result (<| (\\parser.with_extension quantification) + (\\parser.with_extension argument) + \\parser.any) + not_parameter) + (!expect (^.multi {try.#Success [quantification::binding argument::binding actual]} + (same? not_parameter actual))))) + (_.coverage [\\parser.parameter] + (|> (\\parser.result (<| (\\parser.with_extension quantification) + (\\parser.with_extension argument) + \\parser.parameter) + {.#Parameter 0}) + (!expect {try.#Success [quantification::binding argument::binding _]}))) + (_.coverage [\\parser.argument] + (let [argument? (is (-> Nat Nat Bit) + (function (_ @ expected) + (|> (\\parser.result (<| (\\parser.with_extension quantification) + (\\parser.with_extension argument) + (\\parser.with_extension quantification) + (\\parser.with_extension argument) + (do <>.monad + [env \\parser.env + _ \\parser.any] + (in (\\parser.argument env @)))) + not_parameter) + (!expect (^.multi {try.#Success [_ _ _ _ actual]} + (n.= expected actual))))))] + (and (argument? 0 2) + (argument? 1 3) + (argument? 2 0)))) + (_.coverage [\\parser.wrong_parameter] + (|> (\\parser.result (<| (\\parser.with_extension quantification) + (\\parser.with_extension argument) + (\\parser.this_parameter 1)) + {.#Parameter 0}) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.wrong_parameter error))))) + (_.coverage [\\parser.this_parameter] + (|> (\\parser.result (<| (\\parser.with_extension quantification) + (\\parser.with_extension argument) + (\\parser.this_parameter 0)) + {.#Parameter 0}) + (!expect {try.#Success [quantification::binding argument::binding _]}))) + ))) + +(def test|polymorphic + Test + (do [! random.monad] + [not_polymorphic ..primitive + expected_inputs (at ! each (|>> (n.% 10) ++) random.nat)] + (all _.and + (_.coverage [\\parser.not_polymorphic] + (and (|> (\\parser.result (\\parser.polymorphic \\parser.any) + not_polymorphic) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.not_polymorphic error)))) + (|> (\\parser.result (\\parser.polymorphic \\parser.any) + (/.univ_q 0 not_polymorphic)) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.not_polymorphic error)))))) + (_.coverage [\\parser.polymorphic] + (|> (\\parser.result (\\parser.polymorphic \\parser.any) + (/.univ_q expected_inputs not_polymorphic)) + (!expect (^.multi {try.#Success [g!poly actual_inputs bodyT]} + (and (n.= expected_inputs (list.size actual_inputs)) + (same? not_polymorphic bodyT)))))) + ))) + +(def test|recursive + Test + (do random.monad + [expected ..primitive] + (all _.and + (_.coverage [\\parser.recursive] + (|> (.type_literal (Rec @ expected)) + (\\parser.result (\\parser.recursive \\parser.any)) + (!expect (^.multi {try.#Success [@self actual]} + (/#= expected actual))))) + (_.coverage [\\parser.recursive_self] + (|> (.type_literal (Rec @ @)) + (\\parser.result (\\parser.recursive \\parser.recursive_self)) + (!expect (^.multi {try.#Success [@expected @actual]} + (same? @expected @actual))))) + (_.coverage [\\parser.recursive_call] + (|> (.type_literal (All (self input) (self input))) + (\\parser.result (\\parser.polymorphic \\parser.recursive_call)) + (!expect {try.#Success [@self inputs ???]}))) + (_.coverage [\\parser.not_recursive] + (and (|> expected + (\\parser.result (\\parser.recursive \\parser.any)) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.not_recursive error)))) + (|> expected + (\\parser.result \\parser.recursive_self) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.not_recursive error)))))) + ))) + +(def \\parser + Test + (<| (_.covering \\parser._) + (_.for [\\parser.Parser]) + (all _.and + (do [! random.monad] + [expected ..primitive] + (_.coverage [\\parser.result \\parser.any] + (|> (\\parser.result \\parser.any expected) + (!expect (^.multi {try.#Success actual} + (/#= expected actual)))))) + (do [! random.monad] + [expected ..primitive] + (_.coverage [\\parser.next \\parser.unconsumed_input] + (and (|> (\\parser.result (do <>.monad + [actual \\parser.next + _ \\parser.any] + (in actual)) + expected) + (!expect (^.multi {try.#Success actual} + (/#= expected actual)))) + (|> (\\parser.result \\parser.next expected) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.unconsumed_input error))))))) + (do [! random.monad] + [expected ..primitive] + (_.coverage [\\parser.empty_input] + (`` (and (~~ (with_template [] + [(|> (\\parser.result (do <>.monad + [_ \\parser.any] + ) + expected) + (!expect (^.multi {try.#Failure error} + (exception.match? \\parser.empty_input error))))] + + [\\parser.any] + [\\parser.next] + )))))) + (do [! random.monad] + [expected ..primitive] + (_.coverage [\\parser.Env \\parser.env \\parser.fresh] + (|> (\\parser.result (do <>.monad + [env \\parser.env + _ \\parser.any] + (in env)) + expected) + (!expect (^.multi {try.#Success environment} + (same? \\parser.fresh environment)))))) + (do [! random.monad] + [expected ..primitive + dummy (random.only (|>> (/#= expected) not) + ..primitive)] + (_.coverage [\\parser.local] + (|> (\\parser.result (do <>.monad + [_ \\parser.any] + (\\parser.local (list expected) + \\parser.any)) + dummy) + (!expect (^.multi {try.#Success actual} + (/#= expected actual)))))) + (do [! random.monad] + [expected random.nat] + (_.coverage [\\parser.existential \\parser.not_existential] + (|> (\\parser.result \\parser.existential + {.#Ex expected}) + (!expect (^.multi {try.#Success actual} + (n.= expected actual)))))) + (do [! random.monad] + [expected_name (random.and (random.alpha_numeric 1) + (random.alpha_numeric 1)) + expected_type ..primitive] + (_.coverage [\\parser.named \\parser.not_named] + (|> (\\parser.result \\parser.named + {.#Named expected_name expected_type}) + (!expect (^.multi {try.#Success [actual_name actual_type]} + (and (symbol#= expected_name actual_name) + (/#= expected_type actual_type))))))) + ..test|aggregate + ..test|matches + ..test|parameter + ..test|polymorphic + ..test|recursive + ))) + +(def short + (Random Text) + (do [! random.monad] + [size (|> random.nat (at ! each (n.% 10)))] + (random.unicode size))) + +(def symbol + (Random Symbol) + (random.and ..short ..short)) + +(def (random' parameters) + (-> Nat (Random Type)) + (random.rec + (function (_ again) + (let [pairG (random.and again again) + un_parameterized (is (Random Type) + (all random.either + (random#each (|>> {.#Primitive}) (random.and ..short (random.list 0 again))) + (random#each (|>> {.#Primitive}) (random.and ..short (random.list 1 again))) + (random#each (|>> {.#Primitive}) (random.and ..short (random.list 2 again))) + (random#each (|>> {.#Sum}) pairG) + (random#each (|>> {.#Product}) pairG) + (random#each (|>> {.#Function}) pairG) + ))] + (case parameters + 0 un_parameterized + _ (|> random.nat + (random#each (|>> (n.% parameters) {.#Parameter})) + (random.either un_parameterized))))))) + +(def .public (random parameters) + (-> Nat (Random Type)) + (all random.either + (random#each (/.univ_q parameters) (random' parameters)) + (random#each (/.ex_q parameters) (random' parameters)) + )) + +(def .public test + Test + (<| (_.covering /._) + (all _.and + (_.for [/.equivalence] + ($equivalence.spec /.equivalence (..random 0))) + + (do [! random.monad] + [anonymousT (random.only (|>> (pipe.case {.#Named _ _} false + _ true)) + (..random 0)) + symbol/0 ..symbol + symbol/1 ..symbol + .let [namedT {.#Named symbol/0 anonymousT} + aliasedT {.#Named symbol/1 namedT}]] + (all _.and + (_.coverage [/.de_aliased] + (at /.equivalence = namedT (/.de_aliased aliasedT))) + (_.coverage [/.anonymous] + (at /.equivalence = anonymousT (/.anonymous aliasedT))))) + (do [! random.monad] + [size (|> random.nat (at ! each (n.% 3))) + members (|> (..random 0) + (random.only (function (_ type) + (case type + (^.or {.#Sum _} {.#Product _}) + #0 + + _ + #1))) + (list.repeated size) + (monad.all !)) + .let [(open "/#[0]") /.equivalence + (open "list#[0]") (list.equivalence /.equivalence)]] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage [ ] + (let [flat (|> members )] + (or (list#= members flat) + (and (list#= (list) members) + (list#= (list ) flat)))))] + + [/.variant /.flat_variant Nothing] + [/.tuple /.flat_tuple Any] + )) + ))) + (_.coverage [/.applied] + (and (<| (maybe.else #0) + (do maybe.monad + [partial (/.applied (list Bit) Ann) + full (/.applied (list Int) partial)] + (in (at /.equivalence = full {.#Product Bit Int})))) + (|> (/.applied (list Bit) Text) + (pipe.case {.#None} #1 _ #0)))) + (do [! random.monad] + [size (|> random.nat (at ! each (n.% 3))) + members (monad.all ! (list.repeated size (..random 0))) + extra (|> (..random 0) + (random.only (function (_ type) + (case type + (^.or {.#Function _} {.#Apply _}) + #0 + + _ + #1)))) + .let [(open "/#[0]") /.equivalence + (open "list#[0]") (list.equivalence /.equivalence)]] + (all _.and + (_.coverage [/.function /.flat_function] + (let [[inputs output] (|> (/.function members extra) /.flat_function)] + (and (list#= members inputs) + (/#= extra output)))) + (_.coverage [/.application /.flat_application] + (let [[tfunc tparams] (|> extra (/.application members) /.flat_application)] + (n.= (list.size members) (list.size tparams)))) + )) + (do [! random.monad] + [size (|> random.nat (at ! each (|>> (n.% 3) ++))) + body_type (|> (..random 0) + (random.only (function (_ type) + (case type + (^.or {.#UnivQ _} {.#ExQ _}) + #0 + + _ + #1)))) + .let [(open "/#[0]") /.equivalence]] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage [ ] + (let [[flat_size flat_body] (|> body_type ( size) )] + (and (n.= size flat_size) + (/#= body_type flat_body))))] + + [/.univ_q /.flat_univ_q] + [/.ex_q /.flat_ex_q] + )) + (_.coverage [/.quantified?] + (and (not (/.quantified? body_type)) + (|> body_type (/.univ_q size) /.quantified?) + (|> body_type (/.ex_q size) /.quantified?))) + ))) + (do [! random.monad] + [depth (|> random.nat (at ! each (|>> (n.% 3) ++))) + element_type (|> (..random 0) + (random.only (function (_ type) + (case type + (pattern {.#Primitive name (list element_type)}) + (not (text#= array.type_name name)) + + _ + #1)))) + .let [(open "/#[0]") /.equivalence]] + (all _.and + (_.coverage [/.array /.flat_array] + (let [[flat_depth flat_element] (|> element_type (/.array depth) /.flat_array)] + (and (n.= depth flat_depth) + (/#= element_type flat_element)))) + (_.coverage [/.array?] + (and (not (/.array? element_type)) + (/.array? (/.array depth element_type)))) + )) + (_.coverage [/.by_example] + (let [example (is (Maybe Nat) + {.#None})] + (/#= (.type_literal (List Nat)) + (/.by_example [a] + (is (Maybe a) + example) + (List a))))) + (do random.monad + [sample random.nat] + (_.coverage [/.log!] + (exec + (/.log! sample) + true))) + (do random.monad + [left random.nat + right (random.lower_case 1) + .let [left,right [left right]]] + (_.coverage [/.as] + (|> left,right + (/.as [l r] (And l r) (Or l r)) + (/.as [l r] (Or l r) (And l r)) + (same? left,right)))) + (do random.monad + [expected random.nat] + (_.coverage [/.sharing] + (n.= expected + (/.sharing [a] + (is (I64 a) + expected) + (is (I64 a) + (.i64 expected)))))) + (do random.monad + [expected_left random.nat + expected_right random.nat] + (_.coverage [/.let] + (let [[actual_left actual_right] + (is (/.let [side /.Nat] + [side side]) + [expected_left expected_right])] + (and (same? expected_left actual_left) + (same? expected_right actual_right))))) + (do random.monad + [.let [(open "/#[0]") /.equivalence] + left (..random 0) + right (..random 0)] + (all _.and + (_.coverage [/.code] + (bit#= (/#= left right) + (code#= (/.code left) (/.code right)))) + (_.coverage [/.format] + (bit#= (/#= left right) + (text#= (/.format left) (/.format right)))) + )) + + ..\\parser + + /primitive.test + /check.test + /dynamic.test + /implicit.test + /quotient.test + /refinement.test + /resource.test + /unit.test + /variance.test + ))) diff --git a/stdlib/source/test/lux/meta/type/check.lux b/stdlib/source/test/lux/meta/type/check.lux new file mode 100644 index 000000000..b630d37a1 --- /dev/null +++ b/stdlib/source/test/lux/meta/type/check.lux @@ -0,0 +1,900 @@ +(.require + [library + [lux (.except symbol type) + ["_" test (.only Test)] + [abstract + ["[0]" monad (.only do)] + [\\specification + ["$[0]" functor (.only Injection Comparison)] + ["$[0]" apply] + ["$[0]" monad]]] + [control + ["[0]" pipe] + ["[0]" function] + ["[0]" try] + ["[0]" exception (.only exception)]] + [data + ["[0]" bit (.use "[1]#[0]" equivalence)] + ["[0]" product] + ["[0]" text (.use "[1]#[0]" equivalence) + ["%" \\format (.only format)]] + [collection + ["[0]" list (.use "[1]#[0]" functor monoid)] + ["[0]" set]]] + [macro + ["^" pattern]] + [math + ["[0]" random (.only Random) (.use "[1]#[0]" monad)] + [number + ["n" nat]]]]] + [\\library + ["[0]" / (.only) + ["/[1]" // (.use "[1]#[0]" equivalence)]]]) + +... TODO: Remove the following 3 definitions ASAP. //.type already exists... +(def short + (Random Text) + (random.unicode 10)) + +(def symbol + (Random Symbol) + (random.and ..short ..short)) + +(def (type' num_vars) + (-> Nat (Random Type)) + (random.rec + (function (_ again) + (let [pairG (random.and again again) + quantifiedG (random.and (random#in (list)) (type' (++ num_vars))) + random_pair (random.either (random.either (random#each (|>> {.#Sum}) pairG) + (random#each (|>> {.#Product}) pairG)) + (random.either (random#each (|>> {.#Function}) pairG) + (random#each (|>> {.#Apply}) pairG))) + random_id (let [random_id (random.either (random#each (|>> {.#Var}) random.nat) + (random#each (|>> {.#Ex}) random.nat))] + (case num_vars + 0 random_id + _ (random.either (random#each (|>> (n.% num_vars) (n.* 2) ++ {.#Parameter}) random.nat) + random_id))) + random_quantified (random.either (random#each (|>> {.#UnivQ}) quantifiedG) + (random#each (|>> {.#ExQ}) quantifiedG))] + (all random.either + (random#each (|>> {.#Primitive}) (random.and ..short (random#in (list)))) + random_pair + random_id + random_quantified + (random#each (|>> {.#Named}) (random.and ..symbol (type' 0))) + ))))) + +(def type + (Random Type) + (..type' 0)) + +(def (valid_type? type) + (-> Type Bit) + (case type + {.#Primitive name params} + (list.every? valid_type? params) + + {.#Ex id} + #1 + + (^.with_template [] + [{ left right} + (and (valid_type? left) + (valid_type? right))]) + ([.#Sum] [.#Product] [.#Function]) + + {.#Named name type'} + (valid_type? type') + + _ + #0)) + +(def injection + (Injection (All (_ a) (/.Check a))) + (at /.monad in)) + +(def comparison + (Comparison (All (_ a) (/.Check a))) + (function (_ == left right) + (case [(/.result /.fresh_context left) (/.result /.fresh_context right)] + [{try.#Success left} {try.#Success right}] + (== left right) + + _ + false))) + +(def polymorphism + Test + (all _.and + (_.for [/.functor] + ($functor.spec ..injection ..comparison /.functor)) + (_.for [/.apply] + ($apply.spec ..injection ..comparison /.apply)) + (_.for [/.monad] + ($monad.spec ..injection ..comparison /.monad)) + )) + +(def (primitive_type parameters) + (-> Nat (Random Type)) + (do random.monad + [primitive (random.upper_case 3) + parameters (random.list parameters (primitive_type (-- parameters)))] + (in {.#Primitive primitive parameters}))) + +(def clean_type + (Random Type) + (primitive_type 2)) + +(exception yolo) + +(def error_handling + Test + (do random.monad + [left ..clean_type + right ..clean_type + ex random.nat] + (all _.and + (do random.monad + [expected (random.upper_case 10)] + (_.coverage [/.failure] + (case (/.result /.fresh_context + (is (/.Check Any) + (/.failure expected))) + {try.#Success _} false + {try.#Failure actual} (same? expected actual)))) + (do random.monad + [expected (random.upper_case 10)] + (_.coverage [/.assertion] + (and (case (/.result /.fresh_context + (is (/.Check Any) + (/.assertion expected true))) + {try.#Success _} true + {try.#Failure actual} false) + (case (/.result /.fresh_context (/.assertion expected false)) + {try.#Success _} false + {try.#Failure actual} (same? expected actual))))) + (_.coverage [/.except] + (case (/.result /.fresh_context + (is (/.Check Any) + (/.except ..yolo []))) + {try.#Success _} false + {try.#Failure error} (exception.match? ..yolo error))) + (let [scenario (is (-> (-> Text Bit) Type Type Bit) + (function (_ ? ) + (and (|> (/.check ) + (is (/.Check Any)) + (/.result /.fresh_context) + (pipe.case {try.#Failure error} (? error) + {try.#Success _} false)) + (|> (/.check ) + (is (/.Check Any)) + (/.result /.fresh_context) + (pipe.case {try.#Failure error} (? error) + {try.#Success _} false)))))] + (all _.and + (_.coverage [/.type_check_failed] + (let [scenario (scenario (exception.match? /.type_check_failed))] + (and (scenario (Tuple left right) left) + (scenario (Tuple left right) (Or left right)) + (scenario (Tuple left right) (-> left right)) + (scenario (Tuple left right) {.#Ex ex}) + + (scenario (Or left right) left) + (scenario (Or left right) (-> left right)) + (scenario (Or left right) {.#Ex ex}) + + (scenario (-> left right) left) + (scenario (-> left right) {.#Ex ex}) + + (scenario {.#Ex ex} left) + ))) + (_.coverage [/.invalid_type_application] + (let [scenario (scenario (text.contains? (the exception.#label /.invalid_type_application)))] + (scenario {.#Apply left right} left))))) + ))) + +(def var + Test + (<| (_.for [/.Var]) + (all _.and + (_.coverage [/.var] + (case (/.result /.fresh_context + (do /.monad + [[var_id var_type] /.var] + (in (//#= var_type {.#Var var_id})))) + {try.#Success verdict} verdict + {try.#Failure error} false)) + (do random.monad + [nominal (random.upper_case 10)] + (_.coverage [/.bind] + (case (/.result /.fresh_context + (do /.monad + [[var_id var_type] /.var + _ (/.bind {.#Primitive nominal (list)} + var_id)] + (in true))) + {try.#Success _} true + {try.#Failure error} false))) + (do random.monad + [nominal (random.upper_case 10)] + (_.coverage [/.bound?] + (and (|> (do /.monad + [[var_id var_type] /.var + pre (/.bound? var_id) + _ (/.bind {.#Primitive nominal (list)} + var_id) + post (/.bound? var_id)] + (in (and (not pre) + post))) + (/.result /.fresh_context) + (try.else false)) + (|> (do /.monad + [[var_id var/0] /.var + pre (/.bound? var_id) + [_ var/1] /.var + _ (/.check var/0 var/1) + post (/.bound? var_id)] + (in (and (not pre) + (not post)))) + (/.result /.fresh_context) + (try.else false))))) + (do random.monad + [nominal (random.upper_case 10)] + (_.coverage [/.cannot_rebind_var] + (case (/.result /.fresh_context + (do /.monad + [[var_id var_type] /.var + _ (/.bind {.#Primitive nominal (list)} + var_id)] + (/.bind {.#Primitive nominal (list)} + var_id))) + {try.#Success _} + false + + {try.#Failure error} + (exception.match? /.cannot_rebind_var error)))) + (do random.monad + [nominal (random.upper_case 10) + var_id random.nat] + (_.coverage [/.unknown_type_var] + (case (/.result /.fresh_context + (/.bind {.#Primitive nominal (list)} + var_id)) + {try.#Success _} + false + + {try.#Failure error} + (exception.match? /.unknown_type_var error)))) + (do random.monad + [nominal (random.upper_case 10) + .let [expected {.#Primitive nominal (list)}]] + (_.coverage [/.peek] + (and (|> (do /.monad + [[var_id var_type] /.var] + (/.peek var_id)) + (/.result /.fresh_context) + (pipe.case {try.#Success {.#None}} true + _ false)) + (|> (do /.monad + [[var_id var/0] /.var + [_ var/1] /.var + _ (/.check var/0 var/1)] + (/.peek var_id)) + (/.result /.fresh_context) + (pipe.case {try.#Success {.#None}} true + _ false)) + (|> (do /.monad + [[var_id var_type] /.var + _ (/.bind expected var_id)] + (/.peek var_id)) + (/.result /.fresh_context) + (pipe.case {try.#Success {.#Some actual}} + (same? expected actual) + + _ + false))))) + (do random.monad + [nominal (random.upper_case 10) + .let [expected {.#Primitive nominal (list)}]] + (_.coverage [/.read] + (case (/.result /.fresh_context + (do /.monad + [[var_id var_type] /.var + _ (/.bind expected var_id)] + (/.read var_id))) + {try.#Success actual} + (same? expected actual) + + _ + false))) + (do random.monad + [nominal (random.upper_case 10) + .let [expected {.#Primitive nominal (list)}]] + (_.coverage [/.unbound_type_var] + (case (/.result /.fresh_context + (do /.monad + [[var_id var_type] /.var] + (/.read var_id))) + {try.#Failure error} + (exception.match? /.unbound_type_var error) + + _ + false))) + ))) + +(def context + Test + (all _.and + (_.coverage [/.fresh_context] + (and (n.= 0 (the .#var_counter /.fresh_context)) + (n.= 0 (the .#ex_counter /.fresh_context)) + (list.empty? (the .#var_bindings /.fresh_context)))) + (_.coverage [/.context] + (and (case (/.result /.fresh_context /.context) + {try.#Success actual} + (same? /.fresh_context actual) + + {try.#Failure error} + false) + (case (/.result /.fresh_context + (do /.monad + [_ /.var] + /.context)) + {try.#Success actual} + (and (n.= 1 (the .#var_counter actual)) + (n.= 0 (the .#ex_counter actual)) + (n.= 1 (list.size (the .#var_bindings actual)))) + + {try.#Failure error} + false))) + (_.coverage [/.existential] + (case (/.result /.fresh_context + (do /.monad + [_ /.existential] + /.context)) + {try.#Success actual} + (and (n.= 0 (the .#var_counter actual)) + (n.= 1 (the .#ex_counter actual)) + (n.= 0 (list.size (the .#var_bindings actual)))) + + {try.#Failure error} + false)) + )) + +(def succeeds? + (All (_ a) (-> (/.Check a) Bit)) + (|>> (/.result /.fresh_context) + (pipe.case {try.#Success _} + true + + {try.#Failure error} + false))) + +(def fails? + (All (_ a) (-> (/.Check a) Bit)) + (|>> ..succeeds? + not)) + +(def nominal + (Random Type) + (do random.monad + [name (random.upper_case 10)] + (in {.#Primitive name (list)}))) + +(def (non_twins = random) + (All (_ a) (-> (-> a a Bit) (Random a) (Random [a a]))) + (do random.monad + [left random + right (random.only (|>> (= left) not) random)] + (in [left right]))) + +(.type Super + (Ex (_ sub) [Text sub])) + +(.type Sub + (Super Bit)) + +(def (handles_nominal_types! name/0 name/1 parameter/0 parameter/1) + (-> Text Text Type Type Bit) + (let [names_matter! + (and (..succeeds? (/.check {.#Primitive name/0 (list)} + {.#Primitive name/0 (list)})) + (..fails? (/.check {.#Primitive name/0 (list)} + {.#Primitive name/1 (list)}))) + + parameters_matter! + (and (..succeeds? (/.check {.#Primitive name/0 (list parameter/0)} + {.#Primitive name/0 (list parameter/0)})) + (..fails? (/.check {.#Primitive name/0 (list parameter/0)} + {.#Primitive name/0 (list parameter/1)}))) + + covariant_parameters! + (and (..succeeds? (/.check {.#Primitive name/0 (list Super)} + {.#Primitive name/0 (list Sub)})) + (..fails? (/.check {.#Primitive name/0 (list Sub)} + {.#Primitive name/0 (list Super)})))] + (and names_matter! + parameters_matter! + covariant_parameters!))) + +(with_template [ ] + [(def ( name/0 name/1) + (-> Text Text Bit) + (let [pair/0 { {.#Primitive name/0 (list)} {.#Primitive name/0 (list)}} + pair/1 { {.#Primitive name/1 (list)} {.#Primitive name/1 (list)}} + + invariant! + (and (..succeeds? (/.check pair/0 pair/0)) + (..fails? (/.check pair/0 pair/1))) + + super_pair { Super Super} + sub_pair { Sub Sub} + + covariant! + (and (..succeeds? (/.check super_pair sub_pair)) + (..fails? (/.check sub_pair super_pair)))] + (and invariant! + covariant!)))] + + [handles_products! .#Product] + [handles_sums! .#Sum] + ) + +(def (handles_function_variance! nominal) + (-> Type Bit) + (let [functions_have_contravariant_inputs! + (..succeeds? (/.check {.#Function Sub nominal} {.#Function Super nominal})) + + functions_have_covariant_outputs! + (..succeeds? (/.check {.#Function nominal Super} {.#Function nominal Sub}))] + (and functions_have_contravariant_inputs! + functions_have_covariant_outputs!))) + +(def (verdict check) + (All (_ _) (-> (/.Check _) (/.Check Bit))) + (function (_ context) + {try.#Success [context (case (check context) + {try.#Success _} + true + + {try.#Failure _} + false)]})) + +(def (build_ring tail_size) + (-> Nat (/.Check [Type (List Type) Type])) + (do [! /.monad] + [[id/head var/head] /.var + var/tail+ (monad.each ! (function (_ _) + (do ! + [[id/T var/tail] /.var] + (in var/tail))) + (list.repeated tail_size /.var)) + var/last (monad.mix ! (function (_ var/next var/prev) + (do ! + [_ (/.check var/prev var/next)] + (in var/next))) + var/head + var/tail+) + _ (/.check var/last var/head)] + (in [var/head var/tail+ var/last]))) + +(def (handles_var_rings! tail_size nominal/0 nominal/1) + (-> Nat Type Type Bit) + (let [can_create_rings_of_variables! + (succeeds? (..build_ring tail_size)) + + can_bind_rings_of_variables! + (succeeds? (do [! /.monad] + [[var/head var/tail+ var/last] (..build_ring tail_size) + _ (/.check var/head nominal/0) + failures (monad.each ! (|>> (/.check nominal/1) ..verdict) (list.partial var/head var/tail+)) + successes (monad.each ! (|>> (/.check nominal/0) ..verdict) (list.partial var/head var/tail+))] + (/.assertion "" (and (list.every? (bit#= false) failures) + (list.every? (bit#= true) successes))))) + + can_merge_multiple_rings_of_variables! + (succeeds? (do [! /.monad] + [[var/head/0 var/tail+/0 var/last/0] (..build_ring tail_size) + [var/head/1 var/tail+/1 var/last/1] (..build_ring tail_size) + _ (/.check var/head/0 var/head/1) + _ (/.check var/head/0 nominal/0) + .let [all_variables (list#composite (list.partial var/head/0 var/tail+/0) + (list.partial var/head/1 var/tail+/1))] + failures (monad.each ! (|>> (/.check nominal/1) ..verdict) all_variables) + successes (monad.each ! (|>> (/.check nominal/0) ..verdict) all_variables)] + (/.assertion "" (and (list.every? (bit#= false) failures) + (list.every? (bit#= true) successes)))))] + (and can_create_rings_of_variables! + can_bind_rings_of_variables! + can_merge_multiple_rings_of_variables!))) + +(def (handles_vars! nominal) + (-> Type Bit) + (let [vars_check_against_themselves! + (succeeds? (do /.monad + [[id var] /.var] + (/.check var var))) + + can_bind_vars_by_checking_against_them! + (and (succeeds? (do /.monad + [[id var] /.var] + (/.check var nominal))) + (succeeds? (do /.monad + [[id var] /.var] + (/.check nominal var)))) + + cannot_rebind! + (fails? (do /.monad + [[id var] /.var + _ (/.check var nominal)] + (/.check var ..Sub))) + + bound_vars_check_against_their_bound_types! + (and (succeeds? (do /.monad + [[id var] /.var + _ (/.check var nominal)] + (/.check nominal var))) + (succeeds? (do /.monad + [[id var] /.var + _ (/.check var ..Super)] + (/.check var ..Sub))) + (succeeds? (do /.monad + [[id var] /.var + _ (/.check var ..Sub)] + (/.check ..Super var))) + + (fails? (do /.monad + [[id var] /.var + _ (/.check var ..Super)] + (/.check ..Sub var))) + (fails? (do /.monad + [[id var] /.var + _ (/.check var ..Sub)] + (/.check var ..Super))))] + (and vars_check_against_themselves! + can_bind_vars_by_checking_against_them! + cannot_rebind! + bound_vars_check_against_their_bound_types!))) + +(def handles_existentials! + Bit + (let [existentials_always_match_themselves! + (..succeeds? (do /.monad + [[_ single] /.existential] + (/.check single single))) + + existentials_never_match_each_other! + (..fails? (do /.monad + [[_ left] /.existential + [_ right] /.existential] + (/.check left right)))] + (and existentials_always_match_themselves! + existentials_never_match_each_other!))) + +(def (handles_quantification! nominal) + (-> Type Bit) + (let [universals_satisfy_themselves! + (..succeeds? (/.check (.type_literal (All (_ a) (Maybe a))) + (.type_literal (All (_ a) (Maybe a))))) + + existentials_satisfy_themselves! + (..succeeds? (/.check (.type_literal (Ex (_ a) (Maybe a))) + (.type_literal (Ex (_ a) (Maybe a))))) + + universals_satisfy_particulars! + (..succeeds? (/.check (.type_literal (Maybe nominal)) + (.type_literal (All (_ a) (Maybe a))))) + + particulars_do_not_satisfy_universals! + (..fails? (/.check (.type_literal (All (_ a) (Maybe a))) + (.type_literal (Maybe nominal)))) + + particulars_satisfy_existentials! + (..succeeds? (/.check (.type_literal (Ex (_ a) (Maybe a))) + (.type_literal (Maybe nominal)))) + + existentials_do_not_satisfy_particulars! + (..fails? (/.check (.type_literal (Maybe nominal)) + (.type_literal (Ex (_ a) (Maybe a)))))] + (and universals_satisfy_themselves! + existentials_satisfy_themselves! + + universals_satisfy_particulars! + particulars_do_not_satisfy_universals! + + particulars_satisfy_existentials! + existentials_do_not_satisfy_particulars! + ))) + +(def (handles_ultimates! nominal) + (-> Type Bit) + (let [any_is_the_ultimate_super_type! + (and (..succeeds? (/.check Any nominal)) + (..fails? (/.check nominal Any))) + + nothing_is_the_ultimate_sub_type! + (and (..succeeds? (/.check nominal Nothing)) + (..fails? (/.check Nothing nominal))) + + ultimates_check_themselves! + (and (..succeeds? (/.check Any Any)) + (..succeeds? (/.check Nothing Nothing)))] + (and any_is_the_ultimate_super_type! + nothing_is_the_ultimate_sub_type! + ultimates_check_themselves!))) + +(def (names_do_not_affect_types! left_name right_name nominal) + (-> Symbol Symbol Type Bit) + (and (..succeeds? (/.check {.#Named left_name Any} nominal)) + (..succeeds? (/.check Any {.#Named right_name nominal})) + (..succeeds? (/.check {.#Named left_name Any} {.#Named right_name nominal})))) + +... TODO: Test all the crazy corner cases from /.check_apply +(def (handles_application! nominal/0 nominal/1) + (-> Type Type Bit) + (let [types_flow_through! + (and (..succeeds? (/.check (.type_literal ((All (_ a) a) nominal/0)) + nominal/0)) + (..succeeds? (/.check nominal/0 + (.type_literal ((All (_ a) a) nominal/0)))) + + (..succeeds? (/.check (.type_literal ((Ex (_ a) a) nominal/0)) + nominal/0)) + (..succeeds? (/.check nominal/0 + (.type_literal ((Ex (_ a) a) nominal/0))))) + + multiple_parameters! + (and (..succeeds? (/.check (.type_literal ((All (_ a b) [a b]) nominal/0 nominal/1)) + (.type_literal [nominal/0 nominal/1]))) + (..succeeds? (/.check (.type_literal [nominal/0 nominal/1]) + (.type_literal ((All (_ a b) [a b]) nominal/0 nominal/1)))) + + (..succeeds? (/.check (.type_literal ((Ex (_ a b) [a b]) nominal/0 nominal/1)) + (.type_literal [nominal/0 nominal/1]))) + (..succeeds? (/.check (.type_literal [nominal/0 nominal/1]) + (.type_literal ((Ex (_ a b) [a b]) nominal/0 nominal/1)))))] + (and types_flow_through! + multiple_parameters!))) + +(def check + Test + (do [! random.monad] + [nominal ..nominal + [name/0 name/1] (..non_twins text#= (random.upper_case 10)) + [parameter/0 parameter/1] (..non_twins //#= ..nominal) + left_name ..symbol + right_name ..symbol + ring_tail_size (at ! each (n.% 10) random.nat)] + (_.coverage [/.check] + (and (..handles_nominal_types! name/0 name/1 parameter/0 parameter/1) + (..handles_products! name/0 name/1) + (..handles_sums! name/0 name/1) + (..handles_function_variance! nominal) + (..handles_vars! nominal) + (..handles_var_rings! ring_tail_size parameter/0 parameter/1) + ..handles_existentials! + (..handles_quantification! nominal) + (..handles_ultimates! nominal) + (..handles_application! parameter/0 parameter/1) + (..names_do_not_affect_types! left_name right_name nominal) + )))) + +(def dirty_type + (Random (-> Type Type)) + (random.rec + (function (_ dirty_type) + (`` (all random.either + (random#each (function (_ id) + (function.constant {.#Ex id})) + random.nat) + (do random.monad + [module (random.upper_case 10) + short (random.upper_case 10) + anonymousT dirty_type] + (in (function (_ holeT) + {.#Named [module short] (anonymousT holeT)}))) + (~~ (with_template [] + [(do random.monad + [leftT dirty_type + rightT dirty_type] + (in (function (_ holeT) + { (leftT holeT) (rightT holeT)})))] + + [.#Sum] + [.#Product] + [.#Function] + [.#Apply] + )) + (do [! random.monad] + [name (random.upper_case 10) + parameterT dirty_type] + (in (function (_ holeT) + {.#Primitive name (list (parameterT holeT))}))) + (~~ (with_template [] + [(do [! random.monad] + [funcT dirty_type + argT dirty_type + body random.nat] + (in (function (_ holeT) + { (list (funcT holeT) (argT holeT)) + {.#Parameter body}})))] + + [.#UnivQ] + [.#ExQ] + )) + ))))) + +(def clean + Test + (do random.monad + [type_shape ..dirty_type] + (_.coverage [/.clean] + (and (|> (do /.monad + [[var_id varT] /.var + cleanedT (/.clean (list) (type_shape varT))] + (in (//#= (type_shape varT) + cleanedT))) + (/.result /.fresh_context) + (try.else false)) + (|> (do /.monad + [[var_id varT] /.var + [_ replacementT] /.existential + _ (/.check varT replacementT) + cleanedT (/.clean (list) (type_shape varT))] + (in (//#= (type_shape replacementT) + cleanedT))) + (/.result /.fresh_context) + (try.else false)) + )))) + +(def for_subsumption|ultimate + (Random Bit) + (do random.monad + [example ..clean_type] + (in (and (/.subsumes? .Any example) + (not (/.subsumes? example .Any)) + + (/.subsumes? example .Nothing) + (not (/.subsumes? .Nothing example)) + )))) + +(def for_subsumption|nominal + (Random Bit) + (do random.monad + [primitive (random.upper_case 10) + example ..clean_type] + (in (and (/.subsumes? {.#Primitive primitive (list)} + {.#Primitive primitive (list)}) + (/.subsumes? {.#Primitive primitive (list .Any)} + {.#Primitive primitive (list example)}) + (not (/.subsumes? {.#Primitive primitive (list example)} + {.#Primitive primitive (list .Any)})) + (/.subsumes? {.#Primitive primitive (list example)} + {.#Primitive primitive (list .Nothing)}) + (not (/.subsumes? {.#Primitive primitive (list .Nothing)} + {.#Primitive primitive (list example)})) + )))) + +(def for_subsumption|sum + (Random Bit) + (do random.monad + [left ..clean_type + right ..clean_type] + (in (and (/.subsumes? {.#Sum .Any .Any} + {.#Sum left right}) + (not (/.subsumes? {.#Sum left right} + {.#Sum .Any .Any})) + (/.subsumes? {.#Sum left right} + {.#Sum .Nothing .Nothing}) + (not (/.subsumes? {.#Sum .Nothing .Nothing} + {.#Sum left right})) + )))) + +(def for_subsumption|product + (Random Bit) + (do random.monad + [left ..clean_type + right ..clean_type] + (in (and (/.subsumes? {.#Product .Any .Any} + {.#Product left right}) + (not (/.subsumes? {.#Product left right} + {.#Product .Any .Any})) + (/.subsumes? {.#Product left right} + {.#Product .Nothing .Nothing}) + (not (/.subsumes? {.#Product .Nothing .Nothing} + {.#Product left right})) + )))) + +(def for_subsumption|function + (Random Bit) + (do random.monad + [left ..clean_type + right ..clean_type] + (in (and (/.subsumes? {.#Function .Nothing .Any} + {.#Function left right}) + (not (/.subsumes? {.#Function left right} + {.#Function .Nothing .Any})) + (not (/.subsumes? {.#Function .Any .Nothing} + {.#Function left right})) + )))) + +(with_template [ ] + [(def + (Random Bit) + (do random.monad + [id random.nat + example ..clean_type] + (in (not (or (/.subsumes? { id} example) + (/.subsumes? example { id}))))))] + + [.#Var for_subsumption|variable] + [.#Ex for_subsumption|existential] + ) + +(def for_subsumption|quantification+application + (Random Bit) + (do random.monad + [example ..clean_type] + (in (and (and (/.subsumes? (.type_literal (List example)) (.type_literal (All (_ a) (List a)))) + (not (/.subsumes? (.type_literal (All (_ a) (List a))) (.type_literal (List example))))) + (and (/.subsumes? (.type_literal (Ex (_ a) (List a))) (.type_literal (List example))) + (not (/.subsumes? (.type_literal (List example)) (.type_literal (Ex (_ a) (List a)))))))))) + +(def for_subsumption|named + (Random Bit) + (do random.monad + [module (random.upper_case 10) + short (random.upper_case 10) + example ..clean_type] + (in (and (/.subsumes? {.#Named [module short] example} + example) + (/.subsumes? example + {.#Named [module short] example}) + )))) + +(def for_subsumption + Test + (do random.monad + [for_subsumption|ultimate ..for_subsumption|ultimate + for_subsumption|nominal ..for_subsumption|nominal + for_subsumption|sum ..for_subsumption|sum + for_subsumption|product ..for_subsumption|product + for_subsumption|function ..for_subsumption|function + for_subsumption|variable ..for_subsumption|variable + for_subsumption|existential ..for_subsumption|existential + for_subsumption|quantification+application ..for_subsumption|quantification+application + for_subsumption|named ..for_subsumption|named] + (_.coverage [/.subsumes?] + (and for_subsumption|ultimate + for_subsumption|nominal + for_subsumption|sum + for_subsumption|product + for_subsumption|function + for_subsumption|variable + for_subsumption|existential + for_subsumption|quantification+application + for_subsumption|named + )))) + +(def .public test + Test + (<| (_.covering /._) + (_.for [/.Check]) + (all _.and + ..polymorphism + (do random.monad + [expected random.nat] + (_.coverage [/.result] + (case (/.result /.fresh_context + (at /.monad in expected)) + {try.#Success actual} (same? expected actual) + {try.#Failure error} false))) + ..error_handling + ..var + ..context + ..check + ..clean + ..for_subsumption + ))) diff --git a/stdlib/source/test/lux/meta/type/dynamic.lux b/stdlib/source/test/lux/meta/type/dynamic.lux new file mode 100644 index 000000000..595a1da05 --- /dev/null +++ b/stdlib/source/test/lux/meta/type/dynamic.lux @@ -0,0 +1,48 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + [abstract + [monad (.only do)]] + [control + ["[0]" try] + ["[0]" exception]] + [data + ["[0]" text (.use "[1]#[0]" equivalence) + ["%" \\format (.only format)]]] + [math + ["[0]" random (.only Random)] + [number + ["n" nat]]]]] + [\\library + ["[0]" /]]) + +(def .public test + Test + (<| (_.covering /._) + (_.for [/.Dynamic]) + (do random.monad + [expected random.nat] + (all _.and + (_.coverage [/.dynamic /.static] + (case (/.static Nat (/.dynamic expected)) + {try.#Success actual} + (n.= expected actual) + + {try.#Failure _} + false)) + (_.coverage [/.wrong_type] + (case (/.static Text (/.dynamic expected)) + {try.#Success actual} + false + + {try.#Failure error} + (exception.match? /.wrong_type error))) + (_.coverage [/.format] + (case (/.format (/.dynamic expected)) + {try.#Success actual} + (text#= (%.nat expected) actual) + + {try.#Failure _} + false)) + )))) diff --git a/stdlib/source/test/lux/meta/type/implicit.lux b/stdlib/source/test/lux/meta/type/implicit.lux new file mode 100644 index 000000000..299ae7464 --- /dev/null +++ b/stdlib/source/test/lux/meta/type/implicit.lux @@ -0,0 +1,64 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + [abstract + [equivalence (.only)] + [functor (.only)] + [monoid (.only)] + [monad (.only do)] + ["[0]" enum]] + [data + ["[0]" bit (.use "[1]#[0]" equivalence)] + [collection + ["[0]" list]]] + [math + ["[0]" random (.only Random)] + [number + ["n" nat]]]]] + [\\library + ["[0]" /]]) + +(/.implicitly n.multiplication) + +(def .public test + Test + (<| (_.covering /._) + (do [! random.monad] + [.let [digit (at ! each (n.% 10) random.nat)] + left digit + right digit + .let [start (n.min left right) + end (n.max left right)] + + left random.nat + right random.nat] + (all _.and + (_.coverage [/.a/an] + (let [first_order! + (let [(open "list#[0]") (list.equivalence n.equivalence)] + (and (bit#= (at n.equivalence = left right) + (/.a/an = left right)) + (list#= (at list.functor each ++ (enum.range n.enum start end)) + (/.a/an each ++ (enum.range n.enum start end))))) + + second_order! + (/.a/an = + (enum.range n.enum start end) + (enum.range n.enum start end)) + + third_order! + (let [lln (/.a/an each (enum.range n.enum start) + (enum.range n.enum start end))] + (/.a/an = lln lln))] + (and first_order! + second_order! + third_order!))) + (_.coverage [/.with] + (/.with [n.addition] + (n.= (at n.addition composite left right) + (/.a/an composite left right)))) + (_.coverage [/.implicitly] + (n.= (at n.multiplication composite left right) + (/.a/an composite left right))) + )))) diff --git a/stdlib/source/test/lux/meta/type/primitive.lux b/stdlib/source/test/lux/meta/type/primitive.lux new file mode 100644 index 000000000..7b4500c00 --- /dev/null +++ b/stdlib/source/test/lux/meta/type/primitive.lux @@ -0,0 +1,89 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + ["[0]" meta] + [abstract + [monad (.only do)]] + [control + ["[0]" try] + ["[0]" exception]] + [data + ["[0]" text (.use "[1]#[0]" equivalence)]] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["[0]" template] + ["[0]" code (.only) + ["<[1]>" \\parser]]] + ["[0]" math (.only) + ["[0]" random] + [number + ["n" nat]]]]] + [\\library + ["[0]" /]]) + +(template.with_locals [g!Foo g!Bar] + (these (with_template [ ] + [(def + (syntax (_ []) + (do meta.monad + [frame ] + (in (list (code.text (the /.#name frame)))))))] + + [current /.current] + [specific (/.specific (template.text [g!Foo]))] + ) + + (/.primitive (g!Foo a) + Text + + (/.primitive (g!Bar a) + Nat + + (def .public test + Test + (<| (_.covering /._) + (_.for [/.primitive]) + (do random.monad + [expected_foo (random.lower_case 5) + expected_bar random.nat] + (all _.and + (_.coverage [/.abstraction] + (and (exec (is (g!Foo Text) + (/.abstraction g!Foo expected_foo)) + true) + (exec (is (g!Bar Text) + (/.abstraction expected_bar)) + true))) + (_.coverage [/.representation] + (and (|> expected_foo + (/.abstraction g!Foo) + (is (g!Foo Bit)) + (/.representation g!Foo) + (text#= expected_foo)) + (|> (/.abstraction expected_bar) + (is (g!Bar Bit)) + /.representation + (n.= expected_bar)))) + (_.coverage [/.transmutation] + (and (exec (|> expected_foo + (/.abstraction g!Foo) + (is (g!Foo .Macro)) + (/.transmutation g!Foo) + (is (g!Foo .Lux))) + true) + (exec (|> (/.abstraction expected_bar) + (is (g!Bar .Macro)) + /.transmutation + (is (g!Bar .Lux))) + true))) + (_.for [/.Frame] + (all _.and + (_.coverage [/.current] + (text#= (template.text [g!Bar]) + (..current))) + (_.coverage [/.specific] + (text#= (template.text [g!Foo]) + (..specific))) + )) + )))))))) diff --git a/stdlib/source/test/lux/meta/type/quotient.lux b/stdlib/source/test/lux/meta/type/quotient.lux new file mode 100644 index 000000000..72d39b19d --- /dev/null +++ b/stdlib/source/test/lux/meta/type/quotient.lux @@ -0,0 +1,60 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + [abstract + ["[0]" monad (.only do)] + [\\specification + ["$[0]" equivalence]]] + [data + ["[0]" text (.use "[1]#[0]" equivalence) + ["%" \\format (.only format)]]] + [math + ["[0]" random (.only Random)] + [number + ["n" nat (.use "[1]#[0]" equivalence)]]]]] + [\\library + ["[0]" /]]) + +(def .public (random class super) + (All (_ t c %) (-> (/.Class t c %) (Random t) (Random (/.Quotient t c %)))) + (at random.monad each (/.quotient class) super)) + +(def mod_10_class + (/.class (|>> (n.% 10) %.nat))) + +(def Mod_10 + (/.type ..mod_10_class)) + +(def .public test + Test + (<| (_.covering /._) + (do random.monad + [modulus (random.only (n.> 0) random.nat) + .let [class (is (-> Nat Text) + (|>> (n.% modulus) %.nat))] + value random.nat] + (all _.and + (_.for [/.equivalence] + ($equivalence.spec (/.equivalence text.equivalence) + (..random (/.class class) random.nat))) + + (_.for [/.Class] + (_.coverage [/.class] + (same? (is Any class) + (is Any (/.class class))))) + (_.for [/.Quotient] + (all _.and + (_.coverage [/.quotient /.value /.label] + (let [quotient (/.quotient (/.class class) value)] + (and (same? value + (/.value quotient)) + (text#= (class value) + (/.label quotient))))) + (_.coverage [/.type] + (exec + (is ..Mod_10 + (/.quotient ..mod_10_class value)) + true)) + )) + )))) diff --git a/stdlib/source/test/lux/meta/type/refinement.lux b/stdlib/source/test/lux/meta/type/refinement.lux new file mode 100644 index 000000000..711d0401f --- /dev/null +++ b/stdlib/source/test/lux/meta/type/refinement.lux @@ -0,0 +1,91 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + [abstract + [monad (.only do)]] + [control + ["[0]" maybe (.use "[1]#[0]" monad)] + [function + [predicate (.only Predicate)]]] + [data + [collection + ["[0]" list (.use "[1]#[0]" functor)]]] + [math + ["[0]" random] + [number + ["n" nat]]]]] + [\\library + ["[0]" /]]) + +(def _refiner + (/.refiner (n.> 123))) + +(def _type + (/.type _refiner)) + +(def .public test + Test + (<| (_.covering /._) + (_.for [/.Refined]) + (do [! random.monad] + [raw random.nat + modulus (at ! each (|>> (n.% 10) (n.+ 2)) random.nat) + .let [predicate (is (Predicate Nat) + (|>> (n.% modulus) (n.= 0)))] + total_raws (at ! each (|>> (n.% 20) ++) random.nat) + raws (random.list total_raws random.nat)] + (all _.and + (_.for [/.Refiner] + (all _.and + (_.coverage [/.refiner] + (case (/.refiner predicate raw) + {.#Some refined} + (predicate raw) + + {.#None} + (not (predicate raw)))) + (_.coverage [/.predicate] + (|> (/.refiner predicate modulus) + (maybe#each (|>> /.predicate (same? predicate))) + (maybe.else false))) + )) + (_.coverage [/.value] + (|> (/.refiner predicate modulus) + (maybe#each (|>> /.value (n.= modulus))) + (maybe.else false))) + (_.coverage [/.lifted] + (and (|> (/.refiner predicate modulus) + (maybe#each (/.lifted (n.+ modulus))) + maybe#conjoint + (maybe#each (|>> /.value (n.= (n.+ modulus modulus)))) + (maybe.else false)) + (|> (/.refiner predicate modulus) + (maybe#each (/.lifted (n.+ (++ modulus)))) + maybe#conjoint + (maybe#each (|>> /.value (n.= (n.+ modulus (++ modulus))))) + (maybe.else false) + not))) + (_.coverage [/.only] + (let [expected (list.only predicate raws) + actual (/.only (/.refiner predicate) raws)] + (and (n.= (list.size expected) + (list.size actual)) + (at (list.equivalence n.equivalence) = + expected + (list#each /.value actual))))) + (_.coverage [/.partition] + (let [expected (list.only predicate raws) + [actual alternative] (/.partition (/.refiner predicate) raws)] + (and (n.= (list.size expected) + (list.size actual)) + (n.= (n.- (list.size expected) total_raws) + (list.size alternative)) + (at (list.equivalence n.equivalence) = + expected + (list#each /.value actual))))) + (_.coverage [/.type] + (exec (is (Maybe .._type) + (.._refiner raw)) + true)) + )))) diff --git a/stdlib/source/test/lux/meta/type/resource.lux b/stdlib/source/test/lux/meta/type/resource.lux new file mode 100644 index 000000000..a23f1cacf --- /dev/null +++ b/stdlib/source/test/lux/meta/type/resource.lux @@ -0,0 +1,191 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + ["[0]" meta] + [abstract + ["[0]" monad (.only) + [indexed (.only do)]]] + [control + ["[0]" io (.only IO)] + ["[0]" try] + ["[0]" exception (.only Exception)] + [concurrency + ["[0]" async (.only Async)]]] + [data + ["[0]" identity (.only Identity)] + ["[0]" text (.use "[1]#[0]" equivalence) + ["%" \\format (.only format)]]] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["[0]" code (.only) + ["<[1]>" \\parser]]] + [math + ["[0]" random]]]] + [\\library + ["[0]" / (.only Res)]]) + +(def pure + Test + (monad.do [! random.monad] + [pre (at ! each %.nat random.nat) + post (at ! each %.nat random.nat) + .let [! identity.monad]] + (_.for [/.Linear /.run! /.monad] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage + (<| (text#= (format pre post)) + (is (Identity Text)) + (/.run! !) + (do (/.monad !) + + (in (format left right)))))] + + [[/.Affine /.Key /.Res /.Ordered /.ordered + /.Relevant /.read] + [res|left (/.ordered ! pre) + res|right (/.ordered ! post) + right (/.read ! res|right) + left (/.read ! res|left)]] + [[/.Commutative /.commutative /.exchange] + [res|left (/.commutative ! pre) + res|right (/.commutative ! post) + _ ((/.exchange [1 0]) !) + left (/.read ! res|left) + right (/.read ! res|right)]] + [[/.group /.un_group] + [res|left (/.commutative ! pre) + res|right (/.commutative ! post) + _ ((/.group 2) !) + _ ((/.un_group 2) !) + right (/.read ! res|right) + left (/.read ! res|left)]] + [[/.lifted] + [left (/.lifted ! pre) + right (/.lifted ! post)]] + )) + ))))) + +(def sync + Test + (monad.do [! random.monad] + [pre (at ! each %.nat random.nat) + post (at ! each %.nat random.nat) + .let [! io.monad]] + (_.for [/.Linear /.run! /.monad] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage + (<| (text#= (format pre post)) + io.run! + (is (IO Text)) + (/.run! !) + (do (/.monad !) + + (in (format left right)))))] + + [[/.Affine /.Key /.Res /.Ordered /.ordered + /.Relevant /.read] + [res|left (/.ordered ! pre) + res|right (/.ordered ! post) + right (/.read ! res|right) + left (/.read ! res|left)]] + [[/.Commutative /.commutative /.exchange] + [res|left (/.commutative ! pre) + res|right (/.commutative ! post) + _ ((/.exchange [1 0]) !) + left (/.read ! res|left) + right (/.read ! res|right)]] + [[/.group /.un_group] + [res|left (/.commutative ! pre) + res|right (/.commutative ! post) + _ ((/.group 2) !) + _ ((/.un_group 2) !) + right (/.read ! res|right) + left (/.read ! res|left)]] + [[/.lifted] + [left (/.lifted ! (io.io pre)) + right (/.lifted ! (io.io post))]] + )) + ))))) + +(def async + Test + (monad.do [! random.monad] + [pre (at ! each %.nat random.nat) + post (at ! each %.nat random.nat) + .let [! async.monad]] + (_.for [/.Linear /.run! /.monad] + (`` (all _.and + (~~ (with_template [ ] + [(in (monad.do ! + [outcome (<| (is (Async Text)) + (/.run! !) + (do (/.monad !) + + (in (format left right))))] + (_.coverage' + (text#= (format pre post) + outcome))))] + + [[/.Affine /.Key /.Res /.Ordered /.ordered + /.Relevant /.read] + [res|left (/.ordered ! pre) + res|right (/.ordered ! post) + right (/.read ! res|right) + left (/.read ! res|left)]] + [[/.Commutative /.commutative /.exchange] + [res|left (/.commutative ! pre) + res|right (/.commutative ! post) + _ ((/.exchange [1 0]) !) + left (/.read ! res|left) + right (/.read ! res|right)]] + [[/.group /.un_group] + [res|left (/.commutative ! pre) + res|right (/.commutative ! post) + _ ((/.group 2) !) + _ ((/.un_group 2) !) + right (/.read ! res|right) + left (/.read ! res|left)]] + [[/.lifted] + [left (/.lifted ! (async.resolved pre)) + right (/.lifted ! (async.resolved post))]] + )) + ))))) + +(def with_error + (syntax (_ [exception .symbol + to_expand .any]) + (monad.do meta.monad + [[_ _ exception] (meta.export exception)] + (function (_ compiler) + {.#Right [compiler + (list (code.bit (case ((macro.single_expansion to_expand) compiler) + {try.#Success _} + false + + {try.#Failure error} + true)))]})))) + +(def .public test + Test + (<| (_.covering /._) + (_.for [/.Procedure]) + (all _.and + ..pure + ..sync + ..async + + (_.coverage [/.amount_cannot_be_zero] + (`` (and (~~ (with_template [] + [(with_error /.amount_cannot_be_zero + ( 0))] + + [/.group] + [/.un_group] + ))))) + (_.coverage [/.index_cannot_be_repeated] + (with_error /.index_cannot_be_repeated + (/.exchange [0 0]))) + ))) diff --git a/stdlib/source/test/lux/meta/type/unit.lux b/stdlib/source/test/lux/meta/type/unit.lux new file mode 100644 index 000000000..b52ddd921 --- /dev/null +++ b/stdlib/source/test/lux/meta/type/unit.lux @@ -0,0 +1,118 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + [abstract + [monad (.only do)] + [equivalence (.only Equivalence)] + [\\specification + ["$[0]" equivalence] + ["$[0]" order] + ["$[0]" enum]]] + [math + ["[0]" random (.only Random)] + [number + ["i" int]]]]] + [\\library + ["[0]" /]] + ["[0]" / + ["[1][0]" scale]]) + +(with_template [ ] + [(def ( range) + (-> Nat (Random (/.Measure Any ))) + (|> random.int + (at random.monad each (i.% (.int range))) + (random.only (|>> (i.= +0) not)) + (at random.monad each (at in))))] + + [meter /.Meter /.meter] + [second /.Second /.second] + ) + +(def polymorphism + Test + (all _.and + (_.for [/.equivalence] + ($equivalence.spec /.equivalence (..meter 1,000))) + (_.for [/.order] + ($order.spec /.order (..meter 1,000))) + (_.for [/.enum] + ($enum.spec /.enum (..meter 1,000))) + )) + +(def what (/.unit [])) +(def What (/.type what)) + +(def unit + Test + (do random.monad + [expected random.int] + (_.for [/.Unit] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage [ ] + (|> expected + (at in) + (at out) + (i.= expected)))] + + [/.Gram /.gram] + [/.Meter /.meter] + [/.Litre /.litre] + [/.Second /.second] + )) + (_.coverage [/.measure /.number] + (|> expected + /.measure + /.number + (i.= expected))) + (_.coverage [/.unit /.type] + (|> expected + (at ..what in) + (is (/.Measure Any What)) + (at ..what out) + (i.= expected))) + ))))) + +(def arithmetic + Test + (do random.monad + [.let [zero (at /.meter in +0) + (open "meter#[0]") (is (Equivalence (/.Measure Any /.Meter)) + /.equivalence)] + left (random.only (|>> (meter#= zero) not) (..meter 1,000)) + right (..meter 1,000) + extra (..second 1,000)] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage [] + (i.= ( (at /.meter out left) (at /.meter out right)) + (at /.meter out ( left right))))] + + [/.+ i.+] + [/.- i.-] + )) + (_.coverage [/.*] + (let [expected (i.* (at /.meter out left) (at /.meter out right)) + actual (/.number (is (/.Measure Any [/.Meter /.Meter]) + (/.* left right)))] + (i.= expected actual))) + (_.coverage [/./] + (|> right + (/.* left) + (/./ left) + (meter#= right))) + )))) + +(def .public test + Test + (<| (_.covering /._) + (_.for [/.Measure]) + (all _.and + ..polymorphism + ..unit + ..arithmetic + + /scale.test + ))) diff --git a/stdlib/source/test/lux/meta/type/unit/scale.lux b/stdlib/source/test/lux/meta/type/unit/scale.lux new file mode 100644 index 000000000..adc3523b5 --- /dev/null +++ b/stdlib/source/test/lux/meta/type/unit/scale.lux @@ -0,0 +1,97 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + ["[0]" meta] + [abstract + [monad (.only do)] + [equivalence (.only Equivalence)]] + [macro + [syntax (.only syntax)] + ["[0]" code]] + [math + ["[0]" random (.only Random)] + [number + ["i" int] + ["[0]" ratio (.use "[1]#[0]" equivalence)]]]]] + [\\library + ["[0]" / (.only) + ["/[1]" //]]]) + +(def natural + (syntax (_ []) + (at meta.monad each + (|>> code.nat list) + meta.seed))) + +(with_expansions [ (..natural) + (..natural)] + (def how (/.scale [ratio.#denominator ratio.#numerator ])) + (def How (/.type how)) + + (def how::from ) + (def how::to ) + ) + +(def .public test + Test + (<| (_.covering /._) + (_.for [/.Scale]) + (do [! random.monad] + [small (|> random.int + (at ! each (i.% +1,000)) + (at ! each (at //.meter in))) + large (|> random.int + (at ! each (i.% +1,000)) + (at ! each (i.* +1,000,000,000)) + (at ! each (at //.meter in))) + .let [(open "meter#[0]") (is (Equivalence (//.Measure Any //.Meter)) + //.equivalence)] + unscaled (|> random.int + (at ! each (i.% +1,000)) + (at ! each (i.* (.int how::to))) + (at ! each (at //.meter in)))] + (`` (all _.and + (~~ (with_template [ ] + [(_.coverage [ ] + (|> small + (at up) + (is (//.Measure //.Meter)) + (at down) + (is (//.Measure Any //.Meter)) + (meter#= small)))] + + [/.Kilo /.kilo] + [/.Mega /.mega] + [/.Giga /.giga] + )) + (~~ (with_template [ ] + [(_.coverage [ ] + (|> large + (at up) + (is (//.Measure //.Meter)) + (at down) + (is (//.Measure Any //.Meter)) + (meter#= large)))] + + [/.Milli /.milli] + [/.Micro /.micro] + [/.Nano /.nano] + )) + (_.coverage [/.re_scaled] + (|> large (is (//.Measure Any //.Meter)) + (at /.kilo up) (is (//.Measure /.Kilo //.Meter)) + (/.re_scaled /.kilo /.milli) (is (//.Measure /.Milli //.Meter)) + (/.re_scaled /.milli /.kilo) (is (//.Measure /.Kilo //.Meter)) + (at /.kilo down) (is (//.Measure Any //.Meter)) + (meter#= large))) + (_.coverage [/.scale /.type] + (and (|> unscaled + (at ..how up) + (is (//.Measure How //.Meter)) + (at ..how down) + (meter#= unscaled)) + (ratio#= [ratio.#denominator ..how::from + ratio.#numerator ..how::to] + (at ..how ratio)))) + ))))) diff --git a/stdlib/source/test/lux/meta/type/variance.lux b/stdlib/source/test/lux/meta/type/variance.lux new file mode 100644 index 000000000..911c68067 --- /dev/null +++ b/stdlib/source/test/lux/meta/type/variance.lux @@ -0,0 +1,35 @@ +(.require + [library + [lux (.except) + ["_" test (.only Test)] + [abstract + [monad (.only do)]] + [math + ["[0]" random (.only Random)]]]] + [\\library + ["[0]" / (.only) + ["/[1]" // (.only) + ["[1][0]" check]]]]) + +(type Super + (Ex (_ sub) [Text sub])) + +(type Sub + (Super Bit)) + +(def .public test + Test + (<| (_.covering /._) + (all _.and + (_.coverage [/.Co] + (and (//check.subsumes? (type_literal (/.Co Super)) (type_literal (/.Co Sub))) + (not (//check.subsumes? (type_literal (/.Co Sub)) (type_literal (/.Co Super)))))) + (_.coverage [/.Contra] + (and (//check.subsumes? (type_literal (/.Contra Sub)) (type_literal (/.Contra Super))) + (not (//check.subsumes? (type_literal (/.Contra Super)) (type_literal (/.Contra Sub)))))) + (_.coverage [/.In] + (and (//check.subsumes? (type_literal (/.In Super)) (type_literal (/.In Super))) + (//check.subsumes? (type_literal (/.In Sub)) (type_literal (/.In Sub))) + (not (//check.subsumes? (type_literal (/.In Sub)) (type_literal (/.In Super)))) + (not (//check.subsumes? (type_literal (/.In Super)) (type_literal (/.In Sub)))))) + ))) diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux index d862aaf5e..987a00507 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux @@ -24,9 +24,9 @@ ["[0]" symbol ["$[1]" \\test]] ["[0]" configuration - ["$[1]" \\test]]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check (.only Check)]]]] + ["$[1]" \\test]] + ["[0]" type (.use "[1]#[0]" equivalence) + ["[0]" check (.only Check)]]]]] [\\library ["[0]" / (.only) ["/[1]" // (.only) diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/scope.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/scope.lux index 8959c72c9..5fb2ad044 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/scope.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/scope.lux @@ -17,8 +17,9 @@ ["[0]" random (.only Random)] [number ["n" nat]]] - ["[0]" type - ["$[1]" \\test]]]] + [meta + ["[0]" type + ["$[1]" \\test]]]]] [\\library ["[0]" / (.only) ["/[1]" // (.only) diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux index b67b6bd4a..805939c68 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux @@ -13,9 +13,9 @@ ["[0]" random (.only Random)]] [meta ["[0]" configuration - ["$[1]" \\test]]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check]]]] + ["$[1]" \\test]] + ["[0]" type (.use "[1]#[0]" equivalence) + ["[0]" check]]]]] [\\library ["[0]" / (.only) ["/[1]" // (.only) diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis.lux index 8e4113010..3c0823345 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis.lux @@ -18,8 +18,9 @@ ["[0]" random] [number ["n" nat]]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check]]]] + [meta + ["[0]" type (.use "[1]#[0]" equivalence) + ["[0]" check]]]]] [\\library ["[0]" / (.only) [// diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux index 8f58207b2..e5254f4b4 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux @@ -15,8 +15,9 @@ ["[0]" code]] [math ["[0]" random]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check]]]] + [meta + ["[0]" type (.use "[1]#[0]" equivalence) + ["[0]" check]]]]] [\\library ["[0]" / (.only) ["/[1]" // (.only) diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux index 0454ecfb0..31e3355f2 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux @@ -29,9 +29,9 @@ ["[0]" symbol (.only) ["$[1]" \\test]] ["[0]" configuration - ["$[1]" \\test]]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check]]]] + ["$[1]" \\test]] + ["[0]" type (.use "[1]#[0]" equivalence) + ["[0]" check]]]]] [\\library ["[0]" / (.only) ["/[1]" // (.only) diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux index 16b3e1b60..1a865d0d6 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux @@ -22,10 +22,10 @@ ["n" nat]]] [meta ["[0]" symbol - ["$[1]" \\test]]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["$[1]" \\test] - ["[0]" check]]]] + ["$[1]" \\test]] + ["[0]" type (.use "[1]#[0]" equivalence) + ["$[1]" \\test] + ["[0]" check]]]]] [\\library ["[0]" / (.only) ["/[1]" // (.only) diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/reference.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/reference.lux index fd64eff38..d55bc1c2b 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/reference.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/reference.lux @@ -13,8 +13,9 @@ ["[0]" text]] [math ["[0]" random]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["$[1]" \\test]]]] + [meta + ["[0]" type (.use "[1]#[0]" equivalence) + ["$[1]" \\test]]]]] [\\library ["[0]" / (.only) ["/[1]" // diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/simple.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/simple.lux index ebc162c9e..5f7769239 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/simple.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/simple.lux @@ -2,7 +2,6 @@ [library [lux (.except) ["_" test (.only Test)] - ["[0]" type (.use "[1]#[0]" equivalence)] [abstract [monad (.only do)]] [control @@ -13,6 +12,7 @@ [math ["[0]" random]] [meta + ["[0]" type (.use "[1]#[0]" equivalence)] ["[0]" configuration ["$[1]" \\test]]]]] [\\library @@ -88,13 +88,13 @@ (`` (all _.and (_.coverage [/.unit] (..analysis state module .Any /.unit - (|>> (pipe.case (pattern (/analysis.unit)) true _ false)))) + (|>> (pipe.case (pattern (/analysis.unit)) true _ false)))) (~~ (with_template [ ] [(do ! [sample ] (_.coverage [] (..analysis state module ( sample) - ((..analysis? ) sample))))] + ((..analysis? ) sample))))] [/.bit .Bit random.bit /analysis.bit] [/.nat .Nat random.nat /analysis.nat] diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux index 19d27a9b6..7507a6da6 100644 --- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux +++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux @@ -14,11 +14,11 @@ ["[0]" atom]]] [data ["[0]" product]] - ["[0]" type (.use "[1]#[0]" equivalence)] [macro ["[0]" code]] [meta - ["[0]" symbol]]] + ["[0]" symbol] + ["[0]" type (.use "[1]#[0]" equivalence)]]] [//// [analysis ["_[0]" primitive]]] diff --git a/stdlib/source/test/lux/type.lux b/stdlib/source/test/lux/type.lux deleted file mode 100644 index 9f753b1d0..000000000 --- a/stdlib/source/test/lux/type.lux +++ /dev/null @@ -1,567 +0,0 @@ -(.require - [library - [lux (.except symbol) - ["_" test (.only Test)] - [abstract - ["[0]" monad (.only do)] - [\\specification - ["$[0]" equivalence]]] - [control - ["<>" parser] - ["[0]" pipe] - ["[0]" maybe] - ["[0]" try] - ["[0]" exception]] - [data - ["[0]" bit (.use "[1]#[0]" equivalence)] - ["[0]" text (.use "[1]#[0]" equivalence) - ["%" \\format (.only format)]] - [collection - ["[0]" list] - ["[0]" array]]] - [macro - ["^" pattern] - ["[0]" code (.use "[1]#[0]" equivalence)]] - [math - ["[0]" random (.only Random) (.use "[1]#[0]" monad)] - [number - ["n" nat]]] - [meta - ["[0]" symbol (.use "[1]#[0]" equivalence)]]]] - ["[0]" \\parser] - [\\library - ["[0]" / (.use "[1]#[0]" equivalence)]] - ["[0]" / - ["[1][0]" primitive] - ["[1][0]" check] - ["[1][0]" dynamic] - ["[1][0]" implicit] - ["[1][0]" quotient] - ["[1][0]" refinement] - ["[1][0]" resource] - ["[1][0]" unit] - ["[1][0]" variance]]) - -(def !expect - (template (_ ) - [(case - - true - - _ - false)])) - -(def primitive - (Random Type) - (|> (random.alpha_numeric 1) - (at random.monad each (function (_ name) - {.#Primitive name (list)})))) - -(def test|matches - Test - (<| (_.for [\\parser.types_do_not_match]) - (do [! random.monad] - [expected ..primitive - dummy (random.only (|>> (/#= expected) not) - ..primitive)]) - (all _.and - (_.coverage [\\parser.exactly] - (and (|> (\\parser.result (\\parser.exactly expected) expected) - (!expect {try.#Success []})) - (|> (\\parser.result (\\parser.exactly expected) dummy) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.types_do_not_match error)))))) - (_.coverage [\\parser.sub] - (and (|> (\\parser.result (\\parser.sub expected) expected) - (!expect {try.#Success []})) - (|> (\\parser.result (\\parser.sub Any) expected) - (!expect {try.#Success []})) - (|> (\\parser.result (\\parser.sub expected) Nothing) - (!expect {try.#Success []})) - (|> (\\parser.result (\\parser.sub expected) dummy) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.types_do_not_match error)))))) - (_.coverage [\\parser.super] - (and (|> (\\parser.result (\\parser.super expected) expected) - (!expect {try.#Success []})) - (|> (\\parser.result (\\parser.super expected) Any) - (!expect {try.#Success []})) - (|> (\\parser.result (\\parser.super Nothing) expected) - (!expect {try.#Success []})) - (|> (\\parser.result (\\parser.super expected) dummy) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.types_do_not_match error)))))) - ))) - -(def test|aggregate - Test - (do [! random.monad] - [expected_left ..primitive - expected_middle ..primitive - expected_right ..primitive] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage [ ] - (and (|> (\\parser.result ( (all <>.and \\parser.any \\parser.any \\parser.any)) - ( (list expected_left expected_middle expected_right))) - (!expect (^.multi {try.#Success [actual_left actual_middle actual_right]} - (and (/#= expected_left actual_left) - (/#= expected_middle actual_middle) - (/#= expected_right actual_right))))) - (|> (\\parser.result ( (all <>.and \\parser.any \\parser.any \\parser.any)) - ( (list expected_left expected_middle expected_right))) - (!expect (^.multi {try.#Failure error} - (exception.match? error))))))] - - [\\parser.variant \\parser.not_variant /.variant /.tuple] - [\\parser.tuple \\parser.not_tuple /.tuple /.variant] - )) - - (_.coverage [\\parser.function \\parser.not_function] - (and (|> (\\parser.result (\\parser.function (all <>.and \\parser.any \\parser.any) \\parser.any) - (/.function (list expected_left expected_middle) expected_right)) - (!expect (^.multi {try.#Success [[actual_left actual_middle] actual_right]} - (and (/#= expected_left actual_left) - (/#= expected_middle actual_middle) - (/#= expected_right actual_right))))) - (|> (\\parser.result (\\parser.function (all <>.and \\parser.any \\parser.any) \\parser.any) - (/.variant (list expected_left expected_middle expected_right))) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.not_function error)))))) - (_.coverage [\\parser.applied \\parser.not_application] - (and (|> (\\parser.result (\\parser.applied (all <>.and \\parser.any \\parser.any \\parser.any)) - (/.application (list expected_middle expected_right) expected_left)) - (!expect (^.multi {try.#Success [actual_left actual_middle actual_right]} - (and (/#= expected_left actual_left) - (/#= expected_middle actual_middle) - (/#= expected_right actual_right))))) - (|> (\\parser.result (\\parser.applied (all <>.and \\parser.any \\parser.any \\parser.any)) - (/.variant (list expected_left expected_middle expected_right))) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.not_application error)))))) - )))) - -(def test|parameter - Test - (do random.monad - [quantification ..primitive - argument ..primitive - not_parameter ..primitive - parameter random.nat] - (all _.and - (_.coverage [\\parser.not_parameter] - (|> (\\parser.result \\parser.parameter not_parameter) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.not_parameter error))))) - (_.coverage [\\parser.unknown_parameter] - (|> (\\parser.result \\parser.parameter {.#Parameter parameter}) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.unknown_parameter error))))) - (_.coverage [\\parser.with_extension] - (|> (\\parser.result (<| (\\parser.with_extension quantification) - (\\parser.with_extension argument) - \\parser.any) - not_parameter) - (!expect (^.multi {try.#Success [quantification::binding argument::binding actual]} - (same? not_parameter actual))))) - (_.coverage [\\parser.parameter] - (|> (\\parser.result (<| (\\parser.with_extension quantification) - (\\parser.with_extension argument) - \\parser.parameter) - {.#Parameter 0}) - (!expect {try.#Success [quantification::binding argument::binding _]}))) - (_.coverage [\\parser.argument] - (let [argument? (is (-> Nat Nat Bit) - (function (_ @ expected) - (|> (\\parser.result (<| (\\parser.with_extension quantification) - (\\parser.with_extension argument) - (\\parser.with_extension quantification) - (\\parser.with_extension argument) - (do <>.monad - [env \\parser.env - _ \\parser.any] - (in (\\parser.argument env @)))) - not_parameter) - (!expect (^.multi {try.#Success [_ _ _ _ actual]} - (n.= expected actual))))))] - (and (argument? 0 2) - (argument? 1 3) - (argument? 2 0)))) - (_.coverage [\\parser.wrong_parameter] - (|> (\\parser.result (<| (\\parser.with_extension quantification) - (\\parser.with_extension argument) - (\\parser.this_parameter 1)) - {.#Parameter 0}) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.wrong_parameter error))))) - (_.coverage [\\parser.this_parameter] - (|> (\\parser.result (<| (\\parser.with_extension quantification) - (\\parser.with_extension argument) - (\\parser.this_parameter 0)) - {.#Parameter 0}) - (!expect {try.#Success [quantification::binding argument::binding _]}))) - ))) - -(def test|polymorphic - Test - (do [! random.monad] - [not_polymorphic ..primitive - expected_inputs (at ! each (|>> (n.% 10) ++) random.nat)] - (all _.and - (_.coverage [\\parser.not_polymorphic] - (and (|> (\\parser.result (\\parser.polymorphic \\parser.any) - not_polymorphic) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.not_polymorphic error)))) - (|> (\\parser.result (\\parser.polymorphic \\parser.any) - (/.univ_q 0 not_polymorphic)) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.not_polymorphic error)))))) - (_.coverage [\\parser.polymorphic] - (|> (\\parser.result (\\parser.polymorphic \\parser.any) - (/.univ_q expected_inputs not_polymorphic)) - (!expect (^.multi {try.#Success [g!poly actual_inputs bodyT]} - (and (n.= expected_inputs (list.size actual_inputs)) - (same? not_polymorphic bodyT)))))) - ))) - -(def test|recursive - Test - (do random.monad - [expected ..primitive] - (all _.and - (_.coverage [\\parser.recursive] - (|> (.type_literal (Rec @ expected)) - (\\parser.result (\\parser.recursive \\parser.any)) - (!expect (^.multi {try.#Success [@self actual]} - (/#= expected actual))))) - (_.coverage [\\parser.recursive_self] - (|> (.type_literal (Rec @ @)) - (\\parser.result (\\parser.recursive \\parser.recursive_self)) - (!expect (^.multi {try.#Success [@expected @actual]} - (same? @expected @actual))))) - (_.coverage [\\parser.recursive_call] - (|> (.type_literal (All (self input) (self input))) - (\\parser.result (\\parser.polymorphic \\parser.recursive_call)) - (!expect {try.#Success [@self inputs ???]}))) - (_.coverage [\\parser.not_recursive] - (and (|> expected - (\\parser.result (\\parser.recursive \\parser.any)) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.not_recursive error)))) - (|> expected - (\\parser.result \\parser.recursive_self) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.not_recursive error)))))) - ))) - -(def \\parser - Test - (<| (_.covering \\parser._) - (_.for [\\parser.Parser]) - (all _.and - (do [! random.monad] - [expected ..primitive] - (_.coverage [\\parser.result \\parser.any] - (|> (\\parser.result \\parser.any expected) - (!expect (^.multi {try.#Success actual} - (/#= expected actual)))))) - (do [! random.monad] - [expected ..primitive] - (_.coverage [\\parser.next \\parser.unconsumed_input] - (and (|> (\\parser.result (do <>.monad - [actual \\parser.next - _ \\parser.any] - (in actual)) - expected) - (!expect (^.multi {try.#Success actual} - (/#= expected actual)))) - (|> (\\parser.result \\parser.next expected) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.unconsumed_input error))))))) - (do [! random.monad] - [expected ..primitive] - (_.coverage [\\parser.empty_input] - (`` (and (~~ (with_template [] - [(|> (\\parser.result (do <>.monad - [_ \\parser.any] - ) - expected) - (!expect (^.multi {try.#Failure error} - (exception.match? \\parser.empty_input error))))] - - [\\parser.any] - [\\parser.next] - )))))) - (do [! random.monad] - [expected ..primitive] - (_.coverage [\\parser.Env \\parser.env \\parser.fresh] - (|> (\\parser.result (do <>.monad - [env \\parser.env - _ \\parser.any] - (in env)) - expected) - (!expect (^.multi {try.#Success environment} - (same? \\parser.fresh environment)))))) - (do [! random.monad] - [expected ..primitive - dummy (random.only (|>> (/#= expected) not) - ..primitive)] - (_.coverage [\\parser.local] - (|> (\\parser.result (do <>.monad - [_ \\parser.any] - (\\parser.local (list expected) - \\parser.any)) - dummy) - (!expect (^.multi {try.#Success actual} - (/#= expected actual)))))) - (do [! random.monad] - [expected random.nat] - (_.coverage [\\parser.existential \\parser.not_existential] - (|> (\\parser.result \\parser.existential - {.#Ex expected}) - (!expect (^.multi {try.#Success actual} - (n.= expected actual)))))) - (do [! random.monad] - [expected_name (random.and (random.alpha_numeric 1) - (random.alpha_numeric 1)) - expected_type ..primitive] - (_.coverage [\\parser.named \\parser.not_named] - (|> (\\parser.result \\parser.named - {.#Named expected_name expected_type}) - (!expect (^.multi {try.#Success [actual_name actual_type]} - (and (symbol#= expected_name actual_name) - (/#= expected_type actual_type))))))) - ..test|aggregate - ..test|matches - ..test|parameter - ..test|polymorphic - ..test|recursive - ))) - -(def short - (Random Text) - (do [! random.monad] - [size (|> random.nat (at ! each (n.% 10)))] - (random.unicode size))) - -(def symbol - (Random Symbol) - (random.and ..short ..short)) - -(def (random' parameters) - (-> Nat (Random Type)) - (random.rec - (function (_ again) - (let [pairG (random.and again again) - un_parameterized (is (Random Type) - (all random.either - (random#each (|>> {.#Primitive}) (random.and ..short (random.list 0 again))) - (random#each (|>> {.#Primitive}) (random.and ..short (random.list 1 again))) - (random#each (|>> {.#Primitive}) (random.and ..short (random.list 2 again))) - (random#each (|>> {.#Sum}) pairG) - (random#each (|>> {.#Product}) pairG) - (random#each (|>> {.#Function}) pairG) - ))] - (case parameters - 0 un_parameterized - _ (|> random.nat - (random#each (|>> (n.% parameters) {.#Parameter})) - (random.either un_parameterized))))))) - -(def .public (random parameters) - (-> Nat (Random Type)) - (all random.either - (random#each (/.univ_q parameters) (random' parameters)) - (random#each (/.ex_q parameters) (random' parameters)) - )) - -(def .public test - Test - (<| (_.covering /._) - (all _.and - (_.for [/.equivalence] - ($equivalence.spec /.equivalence (..random 0))) - - (do [! random.monad] - [anonymousT (random.only (|>> (pipe.case {.#Named _ _} false - _ true)) - (..random 0)) - symbol/0 ..symbol - symbol/1 ..symbol - .let [namedT {.#Named symbol/0 anonymousT} - aliasedT {.#Named symbol/1 namedT}]] - (all _.and - (_.coverage [/.de_aliased] - (at /.equivalence = namedT (/.de_aliased aliasedT))) - (_.coverage [/.anonymous] - (at /.equivalence = anonymousT (/.anonymous aliasedT))))) - (do [! random.monad] - [size (|> random.nat (at ! each (n.% 3))) - members (|> (..random 0) - (random.only (function (_ type) - (case type - (^.or {.#Sum _} {.#Product _}) - #0 - - _ - #1))) - (list.repeated size) - (monad.all !)) - .let [(open "/#[0]") /.equivalence - (open "list#[0]") (list.equivalence /.equivalence)]] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage [ ] - (let [flat (|> members )] - (or (list#= members flat) - (and (list#= (list) members) - (list#= (list ) flat)))))] - - [/.variant /.flat_variant Nothing] - [/.tuple /.flat_tuple Any] - )) - ))) - (_.coverage [/.applied] - (and (<| (maybe.else #0) - (do maybe.monad - [partial (/.applied (list Bit) Ann) - full (/.applied (list Int) partial)] - (in (at /.equivalence = full {.#Product Bit Int})))) - (|> (/.applied (list Bit) Text) - (pipe.case {.#None} #1 _ #0)))) - (do [! random.monad] - [size (|> random.nat (at ! each (n.% 3))) - members (monad.all ! (list.repeated size (..random 0))) - extra (|> (..random 0) - (random.only (function (_ type) - (case type - (^.or {.#Function _} {.#Apply _}) - #0 - - _ - #1)))) - .let [(open "/#[0]") /.equivalence - (open "list#[0]") (list.equivalence /.equivalence)]] - (all _.and - (_.coverage [/.function /.flat_function] - (let [[inputs output] (|> (/.function members extra) /.flat_function)] - (and (list#= members inputs) - (/#= extra output)))) - (_.coverage [/.application /.flat_application] - (let [[tfunc tparams] (|> extra (/.application members) /.flat_application)] - (n.= (list.size members) (list.size tparams)))) - )) - (do [! random.monad] - [size (|> random.nat (at ! each (|>> (n.% 3) ++))) - body_type (|> (..random 0) - (random.only (function (_ type) - (case type - (^.or {.#UnivQ _} {.#ExQ _}) - #0 - - _ - #1)))) - .let [(open "/#[0]") /.equivalence]] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage [ ] - (let [[flat_size flat_body] (|> body_type ( size) )] - (and (n.= size flat_size) - (/#= body_type flat_body))))] - - [/.univ_q /.flat_univ_q] - [/.ex_q /.flat_ex_q] - )) - (_.coverage [/.quantified?] - (and (not (/.quantified? body_type)) - (|> body_type (/.univ_q size) /.quantified?) - (|> body_type (/.ex_q size) /.quantified?))) - ))) - (do [! random.monad] - [depth (|> random.nat (at ! each (|>> (n.% 3) ++))) - element_type (|> (..random 0) - (random.only (function (_ type) - (case type - (pattern {.#Primitive name (list element_type)}) - (not (text#= array.type_name name)) - - _ - #1)))) - .let [(open "/#[0]") /.equivalence]] - (all _.and - (_.coverage [/.array /.flat_array] - (let [[flat_depth flat_element] (|> element_type (/.array depth) /.flat_array)] - (and (n.= depth flat_depth) - (/#= element_type flat_element)))) - (_.coverage [/.array?] - (and (not (/.array? element_type)) - (/.array? (/.array depth element_type)))) - )) - (_.coverage [/.by_example] - (let [example (is (Maybe Nat) - {.#None})] - (/#= (.type_literal (List Nat)) - (/.by_example [a] - (is (Maybe a) - example) - (List a))))) - (do random.monad - [sample random.nat] - (_.coverage [/.log!] - (exec - (/.log! sample) - true))) - (do random.monad - [left random.nat - right (random.lower_case 1) - .let [left,right [left right]]] - (_.coverage [/.as] - (|> left,right - (/.as [l r] (And l r) (Or l r)) - (/.as [l r] (Or l r) (And l r)) - (same? left,right)))) - (do random.monad - [expected random.nat] - (_.coverage [/.sharing] - (n.= expected - (/.sharing [a] - (is (I64 a) - expected) - (is (I64 a) - (.i64 expected)))))) - (do random.monad - [expected_left random.nat - expected_right random.nat] - (_.coverage [/.let] - (let [[actual_left actual_right] - (is (/.let [side /.Nat] - [side side]) - [expected_left expected_right])] - (and (same? expected_left actual_left) - (same? expected_right actual_right))))) - (do random.monad - [.let [(open "/#[0]") /.equivalence] - left (..random 0) - right (..random 0)] - (all _.and - (_.coverage [/.code] - (bit#= (/#= left right) - (code#= (/.code left) (/.code right)))) - (_.coverage [/.format] - (bit#= (/#= left right) - (text#= (/.format left) (/.format right)))) - )) - - ..\\parser - - /primitive.test - /check.test - /dynamic.test - /implicit.test - /quotient.test - /refinement.test - /resource.test - /unit.test - /variance.test - ))) diff --git a/stdlib/source/test/lux/type/check.lux b/stdlib/source/test/lux/type/check.lux deleted file mode 100644 index 89aa98285..000000000 --- a/stdlib/source/test/lux/type/check.lux +++ /dev/null @@ -1,900 +0,0 @@ -(.require - [library - [lux (.except symbol type) - ["_" test (.only Test)] - ["[0]" type (.use "[1]#[0]" equivalence)] - [abstract - ["[0]" monad (.only do)] - [\\specification - ["$[0]" functor (.only Injection Comparison)] - ["$[0]" apply] - ["$[0]" monad]]] - [control - ["[0]" pipe] - ["[0]" function] - ["[0]" try] - ["[0]" exception (.only exception)]] - [data - ["[0]" bit (.use "[1]#[0]" equivalence)] - ["[0]" product] - ["[0]" text (.use "[1]#[0]" equivalence) - ["%" \\format (.only format)]] - [collection - ["[0]" list (.use "[1]#[0]" functor monoid)] - ["[0]" set]]] - [macro - ["^" pattern]] - [math - ["[0]" random (.only Random) (.use "[1]#[0]" monad)] - [number - ["n" nat]]]]] - [\\library - ["[0]" /]]) - -... TODO: Remove the following 3 definitions ASAP. //.type already exists... -(def short - (Random Text) - (random.unicode 10)) - -(def symbol - (Random Symbol) - (random.and ..short ..short)) - -(def (type' num_vars) - (-> Nat (Random Type)) - (random.rec - (function (_ again) - (let [pairG (random.and again again) - quantifiedG (random.and (random#in (list)) (type' (++ num_vars))) - random_pair (random.either (random.either (random#each (|>> {.#Sum}) pairG) - (random#each (|>> {.#Product}) pairG)) - (random.either (random#each (|>> {.#Function}) pairG) - (random#each (|>> {.#Apply}) pairG))) - random_id (let [random_id (random.either (random#each (|>> {.#Var}) random.nat) - (random#each (|>> {.#Ex}) random.nat))] - (case num_vars - 0 random_id - _ (random.either (random#each (|>> (n.% num_vars) (n.* 2) ++ {.#Parameter}) random.nat) - random_id))) - random_quantified (random.either (random#each (|>> {.#UnivQ}) quantifiedG) - (random#each (|>> {.#ExQ}) quantifiedG))] - (all random.either - (random#each (|>> {.#Primitive}) (random.and ..short (random#in (list)))) - random_pair - random_id - random_quantified - (random#each (|>> {.#Named}) (random.and ..symbol (type' 0))) - ))))) - -(def type - (Random Type) - (..type' 0)) - -(def (valid_type? type) - (-> Type Bit) - (case type - {.#Primitive name params} - (list.every? valid_type? params) - - {.#Ex id} - #1 - - (^.with_template [] - [{ left right} - (and (valid_type? left) - (valid_type? right))]) - ([.#Sum] [.#Product] [.#Function]) - - {.#Named name type'} - (valid_type? type') - - _ - #0)) - -(def injection - (Injection (All (_ a) (/.Check a))) - (at /.monad in)) - -(def comparison - (Comparison (All (_ a) (/.Check a))) - (function (_ == left right) - (case [(/.result /.fresh_context left) (/.result /.fresh_context right)] - [{try.#Success left} {try.#Success right}] - (== left right) - - _ - false))) - -(def polymorphism - Test - (all _.and - (_.for [/.functor] - ($functor.spec ..injection ..comparison /.functor)) - (_.for [/.apply] - ($apply.spec ..injection ..comparison /.apply)) - (_.for [/.monad] - ($monad.spec ..injection ..comparison /.monad)) - )) - -(def (primitive_type parameters) - (-> Nat (Random Type)) - (do random.monad - [primitive (random.upper_case 3) - parameters (random.list parameters (primitive_type (-- parameters)))] - (in {.#Primitive primitive parameters}))) - -(def clean_type - (Random Type) - (primitive_type 2)) - -(exception yolo) - -(def error_handling - Test - (do random.monad - [left ..clean_type - right ..clean_type - ex random.nat] - (all _.and - (do random.monad - [expected (random.upper_case 10)] - (_.coverage [/.failure] - (case (/.result /.fresh_context - (is (/.Check Any) - (/.failure expected))) - {try.#Success _} false - {try.#Failure actual} (same? expected actual)))) - (do random.monad - [expected (random.upper_case 10)] - (_.coverage [/.assertion] - (and (case (/.result /.fresh_context - (is (/.Check Any) - (/.assertion expected true))) - {try.#Success _} true - {try.#Failure actual} false) - (case (/.result /.fresh_context (/.assertion expected false)) - {try.#Success _} false - {try.#Failure actual} (same? expected actual))))) - (_.coverage [/.except] - (case (/.result /.fresh_context - (is (/.Check Any) - (/.except ..yolo []))) - {try.#Success _} false - {try.#Failure error} (exception.match? ..yolo error))) - (let [scenario (is (-> (-> Text Bit) Type Type Bit) - (function (_ ? ) - (and (|> (/.check ) - (is (/.Check Any)) - (/.result /.fresh_context) - (pipe.case {try.#Failure error} (? error) - {try.#Success _} false)) - (|> (/.check ) - (is (/.Check Any)) - (/.result /.fresh_context) - (pipe.case {try.#Failure error} (? error) - {try.#Success _} false)))))] - (all _.and - (_.coverage [/.type_check_failed] - (let [scenario (scenario (exception.match? /.type_check_failed))] - (and (scenario (Tuple left right) left) - (scenario (Tuple left right) (Or left right)) - (scenario (Tuple left right) (-> left right)) - (scenario (Tuple left right) {.#Ex ex}) - - (scenario (Or left right) left) - (scenario (Or left right) (-> left right)) - (scenario (Or left right) {.#Ex ex}) - - (scenario (-> left right) left) - (scenario (-> left right) {.#Ex ex}) - - (scenario {.#Ex ex} left) - ))) - (_.coverage [/.invalid_type_application] - (let [scenario (scenario (text.contains? (the exception.#label /.invalid_type_application)))] - (scenario {.#Apply left right} left))))) - ))) - -(def var - Test - (<| (_.for [/.Var]) - (all _.and - (_.coverage [/.var] - (case (/.result /.fresh_context - (do /.monad - [[var_id var_type] /.var] - (in (type#= var_type {.#Var var_id})))) - {try.#Success verdict} verdict - {try.#Failure error} false)) - (do random.monad - [nominal (random.upper_case 10)] - (_.coverage [/.bind] - (case (/.result /.fresh_context - (do /.monad - [[var_id var_type] /.var - _ (/.bind {.#Primitive nominal (list)} - var_id)] - (in true))) - {try.#Success _} true - {try.#Failure error} false))) - (do random.monad - [nominal (random.upper_case 10)] - (_.coverage [/.bound?] - (and (|> (do /.monad - [[var_id var_type] /.var - pre (/.bound? var_id) - _ (/.bind {.#Primitive nominal (list)} - var_id) - post (/.bound? var_id)] - (in (and (not pre) - post))) - (/.result /.fresh_context) - (try.else false)) - (|> (do /.monad - [[var_id var/0] /.var - pre (/.bound? var_id) - [_ var/1] /.var - _ (/.check var/0 var/1) - post (/.bound? var_id)] - (in (and (not pre) - (not post)))) - (/.result /.fresh_context) - (try.else false))))) - (do random.monad - [nominal (random.upper_case 10)] - (_.coverage [/.cannot_rebind_var] - (case (/.result /.fresh_context - (do /.monad - [[var_id var_type] /.var - _ (/.bind {.#Primitive nominal (list)} - var_id)] - (/.bind {.#Primitive nominal (list)} - var_id))) - {try.#Success _} - false - - {try.#Failure error} - (exception.match? /.cannot_rebind_var error)))) - (do random.monad - [nominal (random.upper_case 10) - var_id random.nat] - (_.coverage [/.unknown_type_var] - (case (/.result /.fresh_context - (/.bind {.#Primitive nominal (list)} - var_id)) - {try.#Success _} - false - - {try.#Failure error} - (exception.match? /.unknown_type_var error)))) - (do random.monad - [nominal (random.upper_case 10) - .let [expected {.#Primitive nominal (list)}]] - (_.coverage [/.peek] - (and (|> (do /.monad - [[var_id var_type] /.var] - (/.peek var_id)) - (/.result /.fresh_context) - (pipe.case {try.#Success {.#None}} true - _ false)) - (|> (do /.monad - [[var_id var/0] /.var - [_ var/1] /.var - _ (/.check var/0 var/1)] - (/.peek var_id)) - (/.result /.fresh_context) - (pipe.case {try.#Success {.#None}} true - _ false)) - (|> (do /.monad - [[var_id var_type] /.var - _ (/.bind expected var_id)] - (/.peek var_id)) - (/.result /.fresh_context) - (pipe.case {try.#Success {.#Some actual}} - (same? expected actual) - - _ - false))))) - (do random.monad - [nominal (random.upper_case 10) - .let [expected {.#Primitive nominal (list)}]] - (_.coverage [/.read] - (case (/.result /.fresh_context - (do /.monad - [[var_id var_type] /.var - _ (/.bind expected var_id)] - (/.read var_id))) - {try.#Success actual} - (same? expected actual) - - _ - false))) - (do random.monad - [nominal (random.upper_case 10) - .let [expected {.#Primitive nominal (list)}]] - (_.coverage [/.unbound_type_var] - (case (/.result /.fresh_context - (do /.monad - [[var_id var_type] /.var] - (/.read var_id))) - {try.#Failure error} - (exception.match? /.unbound_type_var error) - - _ - false))) - ))) - -(def context - Test - (all _.and - (_.coverage [/.fresh_context] - (and (n.= 0 (the .#var_counter /.fresh_context)) - (n.= 0 (the .#ex_counter /.fresh_context)) - (list.empty? (the .#var_bindings /.fresh_context)))) - (_.coverage [/.context] - (and (case (/.result /.fresh_context /.context) - {try.#Success actual} - (same? /.fresh_context actual) - - {try.#Failure error} - false) - (case (/.result /.fresh_context - (do /.monad - [_ /.var] - /.context)) - {try.#Success actual} - (and (n.= 1 (the .#var_counter actual)) - (n.= 0 (the .#ex_counter actual)) - (n.= 1 (list.size (the .#var_bindings actual)))) - - {try.#Failure error} - false))) - (_.coverage [/.existential] - (case (/.result /.fresh_context - (do /.monad - [_ /.existential] - /.context)) - {try.#Success actual} - (and (n.= 0 (the .#var_counter actual)) - (n.= 1 (the .#ex_counter actual)) - (n.= 0 (list.size (the .#var_bindings actual)))) - - {try.#Failure error} - false)) - )) - -(def succeeds? - (All (_ a) (-> (/.Check a) Bit)) - (|>> (/.result /.fresh_context) - (pipe.case {try.#Success _} - true - - {try.#Failure error} - false))) - -(def fails? - (All (_ a) (-> (/.Check a) Bit)) - (|>> ..succeeds? - not)) - -(def nominal - (Random Type) - (do random.monad - [name (random.upper_case 10)] - (in {.#Primitive name (list)}))) - -(def (non_twins = random) - (All (_ a) (-> (-> a a Bit) (Random a) (Random [a a]))) - (do random.monad - [left random - right (random.only (|>> (= left) not) random)] - (in [left right]))) - -(.type Super - (Ex (_ sub) [Text sub])) - -(.type Sub - (Super Bit)) - -(def (handles_nominal_types! name/0 name/1 parameter/0 parameter/1) - (-> Text Text Type Type Bit) - (let [names_matter! - (and (..succeeds? (/.check {.#Primitive name/0 (list)} - {.#Primitive name/0 (list)})) - (..fails? (/.check {.#Primitive name/0 (list)} - {.#Primitive name/1 (list)}))) - - parameters_matter! - (and (..succeeds? (/.check {.#Primitive name/0 (list parameter/0)} - {.#Primitive name/0 (list parameter/0)})) - (..fails? (/.check {.#Primitive name/0 (list parameter/0)} - {.#Primitive name/0 (list parameter/1)}))) - - covariant_parameters! - (and (..succeeds? (/.check {.#Primitive name/0 (list Super)} - {.#Primitive name/0 (list Sub)})) - (..fails? (/.check {.#Primitive name/0 (list Sub)} - {.#Primitive name/0 (list Super)})))] - (and names_matter! - parameters_matter! - covariant_parameters!))) - -(with_template [ ] - [(def ( name/0 name/1) - (-> Text Text Bit) - (let [pair/0 { {.#Primitive name/0 (list)} {.#Primitive name/0 (list)}} - pair/1 { {.#Primitive name/1 (list)} {.#Primitive name/1 (list)}} - - invariant! - (and (..succeeds? (/.check pair/0 pair/0)) - (..fails? (/.check pair/0 pair/1))) - - super_pair { Super Super} - sub_pair { Sub Sub} - - covariant! - (and (..succeeds? (/.check super_pair sub_pair)) - (..fails? (/.check sub_pair super_pair)))] - (and invariant! - covariant!)))] - - [handles_products! .#Product] - [handles_sums! .#Sum] - ) - -(def (handles_function_variance! nominal) - (-> Type Bit) - (let [functions_have_contravariant_inputs! - (..succeeds? (/.check {.#Function Sub nominal} {.#Function Super nominal})) - - functions_have_covariant_outputs! - (..succeeds? (/.check {.#Function nominal Super} {.#Function nominal Sub}))] - (and functions_have_contravariant_inputs! - functions_have_covariant_outputs!))) - -(def (verdict check) - (All (_ _) (-> (/.Check _) (/.Check Bit))) - (function (_ context) - {try.#Success [context (case (check context) - {try.#Success _} - true - - {try.#Failure _} - false)]})) - -(def (build_ring tail_size) - (-> Nat (/.Check [Type (List Type) Type])) - (do [! /.monad] - [[id/head var/head] /.var - var/tail+ (monad.each ! (function (_ _) - (do ! - [[id/T var/tail] /.var] - (in var/tail))) - (list.repeated tail_size /.var)) - var/last (monad.mix ! (function (_ var/next var/prev) - (do ! - [_ (/.check var/prev var/next)] - (in var/next))) - var/head - var/tail+) - _ (/.check var/last var/head)] - (in [var/head var/tail+ var/last]))) - -(def (handles_var_rings! tail_size nominal/0 nominal/1) - (-> Nat Type Type Bit) - (let [can_create_rings_of_variables! - (succeeds? (..build_ring tail_size)) - - can_bind_rings_of_variables! - (succeeds? (do [! /.monad] - [[var/head var/tail+ var/last] (..build_ring tail_size) - _ (/.check var/head nominal/0) - failures (monad.each ! (|>> (/.check nominal/1) ..verdict) (list.partial var/head var/tail+)) - successes (monad.each ! (|>> (/.check nominal/0) ..verdict) (list.partial var/head var/tail+))] - (/.assertion "" (and (list.every? (bit#= false) failures) - (list.every? (bit#= true) successes))))) - - can_merge_multiple_rings_of_variables! - (succeeds? (do [! /.monad] - [[var/head/0 var/tail+/0 var/last/0] (..build_ring tail_size) - [var/head/1 var/tail+/1 var/last/1] (..build_ring tail_size) - _ (/.check var/head/0 var/head/1) - _ (/.check var/head/0 nominal/0) - .let [all_variables (list#composite (list.partial var/head/0 var/tail+/0) - (list.partial var/head/1 var/tail+/1))] - failures (monad.each ! (|>> (/.check nominal/1) ..verdict) all_variables) - successes (monad.each ! (|>> (/.check nominal/0) ..verdict) all_variables)] - (/.assertion "" (and (list.every? (bit#= false) failures) - (list.every? (bit#= true) successes)))))] - (and can_create_rings_of_variables! - can_bind_rings_of_variables! - can_merge_multiple_rings_of_variables!))) - -(def (handles_vars! nominal) - (-> Type Bit) - (let [vars_check_against_themselves! - (succeeds? (do /.monad - [[id var] /.var] - (/.check var var))) - - can_bind_vars_by_checking_against_them! - (and (succeeds? (do /.monad - [[id var] /.var] - (/.check var nominal))) - (succeeds? (do /.monad - [[id var] /.var] - (/.check nominal var)))) - - cannot_rebind! - (fails? (do /.monad - [[id var] /.var - _ (/.check var nominal)] - (/.check var ..Sub))) - - bound_vars_check_against_their_bound_types! - (and (succeeds? (do /.monad - [[id var] /.var - _ (/.check var nominal)] - (/.check nominal var))) - (succeeds? (do /.monad - [[id var] /.var - _ (/.check var ..Super)] - (/.check var ..Sub))) - (succeeds? (do /.monad - [[id var] /.var - _ (/.check var ..Sub)] - (/.check ..Super var))) - - (fails? (do /.monad - [[id var] /.var - _ (/.check var ..Super)] - (/.check ..Sub var))) - (fails? (do /.monad - [[id var] /.var - _ (/.check var ..Sub)] - (/.check var ..Super))))] - (and vars_check_against_themselves! - can_bind_vars_by_checking_against_them! - cannot_rebind! - bound_vars_check_against_their_bound_types!))) - -(def handles_existentials! - Bit - (let [existentials_always_match_themselves! - (..succeeds? (do /.monad - [[_ single] /.existential] - (/.check single single))) - - existentials_never_match_each_other! - (..fails? (do /.monad - [[_ left] /.existential - [_ right] /.existential] - (/.check left right)))] - (and existentials_always_match_themselves! - existentials_never_match_each_other!))) - -(def (handles_quantification! nominal) - (-> Type Bit) - (let [universals_satisfy_themselves! - (..succeeds? (/.check (.type_literal (All (_ a) (Maybe a))) - (.type_literal (All (_ a) (Maybe a))))) - - existentials_satisfy_themselves! - (..succeeds? (/.check (.type_literal (Ex (_ a) (Maybe a))) - (.type_literal (Ex (_ a) (Maybe a))))) - - universals_satisfy_particulars! - (..succeeds? (/.check (.type_literal (Maybe nominal)) - (.type_literal (All (_ a) (Maybe a))))) - - particulars_do_not_satisfy_universals! - (..fails? (/.check (.type_literal (All (_ a) (Maybe a))) - (.type_literal (Maybe nominal)))) - - particulars_satisfy_existentials! - (..succeeds? (/.check (.type_literal (Ex (_ a) (Maybe a))) - (.type_literal (Maybe nominal)))) - - existentials_do_not_satisfy_particulars! - (..fails? (/.check (.type_literal (Maybe nominal)) - (.type_literal (Ex (_ a) (Maybe a)))))] - (and universals_satisfy_themselves! - existentials_satisfy_themselves! - - universals_satisfy_particulars! - particulars_do_not_satisfy_universals! - - particulars_satisfy_existentials! - existentials_do_not_satisfy_particulars! - ))) - -(def (handles_ultimates! nominal) - (-> Type Bit) - (let [any_is_the_ultimate_super_type! - (and (..succeeds? (/.check Any nominal)) - (..fails? (/.check nominal Any))) - - nothing_is_the_ultimate_sub_type! - (and (..succeeds? (/.check nominal Nothing)) - (..fails? (/.check Nothing nominal))) - - ultimates_check_themselves! - (and (..succeeds? (/.check Any Any)) - (..succeeds? (/.check Nothing Nothing)))] - (and any_is_the_ultimate_super_type! - nothing_is_the_ultimate_sub_type! - ultimates_check_themselves!))) - -(def (names_do_not_affect_types! left_name right_name nominal) - (-> Symbol Symbol Type Bit) - (and (..succeeds? (/.check {.#Named left_name Any} nominal)) - (..succeeds? (/.check Any {.#Named right_name nominal})) - (..succeeds? (/.check {.#Named left_name Any} {.#Named right_name nominal})))) - -... TODO: Test all the crazy corner cases from /.check_apply -(def (handles_application! nominal/0 nominal/1) - (-> Type Type Bit) - (let [types_flow_through! - (and (..succeeds? (/.check (.type_literal ((All (_ a) a) nominal/0)) - nominal/0)) - (..succeeds? (/.check nominal/0 - (.type_literal ((All (_ a) a) nominal/0)))) - - (..succeeds? (/.check (.type_literal ((Ex (_ a) a) nominal/0)) - nominal/0)) - (..succeeds? (/.check nominal/0 - (.type_literal ((Ex (_ a) a) nominal/0))))) - - multiple_parameters! - (and (..succeeds? (/.check (.type_literal ((All (_ a b) [a b]) nominal/0 nominal/1)) - (.type_literal [nominal/0 nominal/1]))) - (..succeeds? (/.check (.type_literal [nominal/0 nominal/1]) - (.type_literal ((All (_ a b) [a b]) nominal/0 nominal/1)))) - - (..succeeds? (/.check (.type_literal ((Ex (_ a b) [a b]) nominal/0 nominal/1)) - (.type_literal [nominal/0 nominal/1]))) - (..succeeds? (/.check (.type_literal [nominal/0 nominal/1]) - (.type_literal ((Ex (_ a b) [a b]) nominal/0 nominal/1)))))] - (and types_flow_through! - multiple_parameters!))) - -(def check - Test - (do [! random.monad] - [nominal ..nominal - [name/0 name/1] (..non_twins text#= (random.upper_case 10)) - [parameter/0 parameter/1] (..non_twins type#= ..nominal) - left_name ..symbol - right_name ..symbol - ring_tail_size (at ! each (n.% 10) random.nat)] - (_.coverage [/.check] - (and (..handles_nominal_types! name/0 name/1 parameter/0 parameter/1) - (..handles_products! name/0 name/1) - (..handles_sums! name/0 name/1) - (..handles_function_variance! nominal) - (..handles_vars! nominal) - (..handles_var_rings! ring_tail_size parameter/0 parameter/1) - ..handles_existentials! - (..handles_quantification! nominal) - (..handles_ultimates! nominal) - (..handles_application! parameter/0 parameter/1) - (..names_do_not_affect_types! left_name right_name nominal) - )))) - -(def dirty_type - (Random (-> Type Type)) - (random.rec - (function (_ dirty_type) - (`` (all random.either - (random#each (function (_ id) - (function.constant {.#Ex id})) - random.nat) - (do random.monad - [module (random.upper_case 10) - short (random.upper_case 10) - anonymousT dirty_type] - (in (function (_ holeT) - {.#Named [module short] (anonymousT holeT)}))) - (~~ (with_template [] - [(do random.monad - [leftT dirty_type - rightT dirty_type] - (in (function (_ holeT) - { (leftT holeT) (rightT holeT)})))] - - [.#Sum] - [.#Product] - [.#Function] - [.#Apply] - )) - (do [! random.monad] - [name (random.upper_case 10) - parameterT dirty_type] - (in (function (_ holeT) - {.#Primitive name (list (parameterT holeT))}))) - (~~ (with_template [] - [(do [! random.monad] - [funcT dirty_type - argT dirty_type - body random.nat] - (in (function (_ holeT) - { (list (funcT holeT) (argT holeT)) - {.#Parameter body}})))] - - [.#UnivQ] - [.#ExQ] - )) - ))))) - -(def clean - Test - (do random.monad - [type_shape ..dirty_type] - (_.coverage [/.clean] - (and (|> (do /.monad - [[var_id varT] /.var - cleanedT (/.clean (list) (type_shape varT))] - (in (type#= (type_shape varT) - cleanedT))) - (/.result /.fresh_context) - (try.else false)) - (|> (do /.monad - [[var_id varT] /.var - [_ replacementT] /.existential - _ (/.check varT replacementT) - cleanedT (/.clean (list) (type_shape varT))] - (in (type#= (type_shape replacementT) - cleanedT))) - (/.result /.fresh_context) - (try.else false)) - )))) - -(def for_subsumption|ultimate - (Random Bit) - (do random.monad - [example ..clean_type] - (in (and (/.subsumes? .Any example) - (not (/.subsumes? example .Any)) - - (/.subsumes? example .Nothing) - (not (/.subsumes? .Nothing example)) - )))) - -(def for_subsumption|nominal - (Random Bit) - (do random.monad - [primitive (random.upper_case 10) - example ..clean_type] - (in (and (/.subsumes? {.#Primitive primitive (list)} - {.#Primitive primitive (list)}) - (/.subsumes? {.#Primitive primitive (list .Any)} - {.#Primitive primitive (list example)}) - (not (/.subsumes? {.#Primitive primitive (list example)} - {.#Primitive primitive (list .Any)})) - (/.subsumes? {.#Primitive primitive (list example)} - {.#Primitive primitive (list .Nothing)}) - (not (/.subsumes? {.#Primitive primitive (list .Nothing)} - {.#Primitive primitive (list example)})) - )))) - -(def for_subsumption|sum - (Random Bit) - (do random.monad - [left ..clean_type - right ..clean_type] - (in (and (/.subsumes? {.#Sum .Any .Any} - {.#Sum left right}) - (not (/.subsumes? {.#Sum left right} - {.#Sum .Any .Any})) - (/.subsumes? {.#Sum left right} - {.#Sum .Nothing .Nothing}) - (not (/.subsumes? {.#Sum .Nothing .Nothing} - {.#Sum left right})) - )))) - -(def for_subsumption|product - (Random Bit) - (do random.monad - [left ..clean_type - right ..clean_type] - (in (and (/.subsumes? {.#Product .Any .Any} - {.#Product left right}) - (not (/.subsumes? {.#Product left right} - {.#Product .Any .Any})) - (/.subsumes? {.#Product left right} - {.#Product .Nothing .Nothing}) - (not (/.subsumes? {.#Product .Nothing .Nothing} - {.#Product left right})) - )))) - -(def for_subsumption|function - (Random Bit) - (do random.monad - [left ..clean_type - right ..clean_type] - (in (and (/.subsumes? {.#Function .Nothing .Any} - {.#Function left right}) - (not (/.subsumes? {.#Function left right} - {.#Function .Nothing .Any})) - (not (/.subsumes? {.#Function .Any .Nothing} - {.#Function left right})) - )))) - -(with_template [ ] - [(def - (Random Bit) - (do random.monad - [id random.nat - example ..clean_type] - (in (not (or (/.subsumes? { id} example) - (/.subsumes? example { id}))))))] - - [.#Var for_subsumption|variable] - [.#Ex for_subsumption|existential] - ) - -(def for_subsumption|quantification+application - (Random Bit) - (do random.monad - [example ..clean_type] - (in (and (and (/.subsumes? (.type_literal (List example)) (.type_literal (All (_ a) (List a)))) - (not (/.subsumes? (.type_literal (All (_ a) (List a))) (.type_literal (List example))))) - (and (/.subsumes? (.type_literal (Ex (_ a) (List a))) (.type_literal (List example))) - (not (/.subsumes? (.type_literal (List example)) (.type_literal (Ex (_ a) (List a)))))))))) - -(def for_subsumption|named - (Random Bit) - (do random.monad - [module (random.upper_case 10) - short (random.upper_case 10) - example ..clean_type] - (in (and (/.subsumes? {.#Named [module short] example} - example) - (/.subsumes? example - {.#Named [module short] example}) - )))) - -(def for_subsumption - Test - (do random.monad - [for_subsumption|ultimate ..for_subsumption|ultimate - for_subsumption|nominal ..for_subsumption|nominal - for_subsumption|sum ..for_subsumption|sum - for_subsumption|product ..for_subsumption|product - for_subsumption|function ..for_subsumption|function - for_subsumption|variable ..for_subsumption|variable - for_subsumption|existential ..for_subsumption|existential - for_subsumption|quantification+application ..for_subsumption|quantification+application - for_subsumption|named ..for_subsumption|named] - (_.coverage [/.subsumes?] - (and for_subsumption|ultimate - for_subsumption|nominal - for_subsumption|sum - for_subsumption|product - for_subsumption|function - for_subsumption|variable - for_subsumption|existential - for_subsumption|quantification+application - for_subsumption|named - )))) - -(def .public test - Test - (<| (_.covering /._) - (_.for [/.Check]) - (all _.and - ..polymorphism - (do random.monad - [expected random.nat] - (_.coverage [/.result] - (case (/.result /.fresh_context - (at /.monad in expected)) - {try.#Success actual} (same? expected actual) - {try.#Failure error} false))) - ..error_handling - ..var - ..context - ..check - ..clean - ..for_subsumption - ))) diff --git a/stdlib/source/test/lux/type/dynamic.lux b/stdlib/source/test/lux/type/dynamic.lux deleted file mode 100644 index 595a1da05..000000000 --- a/stdlib/source/test/lux/type/dynamic.lux +++ /dev/null @@ -1,48 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - [abstract - [monad (.only do)]] - [control - ["[0]" try] - ["[0]" exception]] - [data - ["[0]" text (.use "[1]#[0]" equivalence) - ["%" \\format (.only format)]]] - [math - ["[0]" random (.only Random)] - [number - ["n" nat]]]]] - [\\library - ["[0]" /]]) - -(def .public test - Test - (<| (_.covering /._) - (_.for [/.Dynamic]) - (do random.monad - [expected random.nat] - (all _.and - (_.coverage [/.dynamic /.static] - (case (/.static Nat (/.dynamic expected)) - {try.#Success actual} - (n.= expected actual) - - {try.#Failure _} - false)) - (_.coverage [/.wrong_type] - (case (/.static Text (/.dynamic expected)) - {try.#Success actual} - false - - {try.#Failure error} - (exception.match? /.wrong_type error))) - (_.coverage [/.format] - (case (/.format (/.dynamic expected)) - {try.#Success actual} - (text#= (%.nat expected) actual) - - {try.#Failure _} - false)) - )))) diff --git a/stdlib/source/test/lux/type/implicit.lux b/stdlib/source/test/lux/type/implicit.lux deleted file mode 100644 index 299ae7464..000000000 --- a/stdlib/source/test/lux/type/implicit.lux +++ /dev/null @@ -1,64 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - [abstract - [equivalence (.only)] - [functor (.only)] - [monoid (.only)] - [monad (.only do)] - ["[0]" enum]] - [data - ["[0]" bit (.use "[1]#[0]" equivalence)] - [collection - ["[0]" list]]] - [math - ["[0]" random (.only Random)] - [number - ["n" nat]]]]] - [\\library - ["[0]" /]]) - -(/.implicitly n.multiplication) - -(def .public test - Test - (<| (_.covering /._) - (do [! random.monad] - [.let [digit (at ! each (n.% 10) random.nat)] - left digit - right digit - .let [start (n.min left right) - end (n.max left right)] - - left random.nat - right random.nat] - (all _.and - (_.coverage [/.a/an] - (let [first_order! - (let [(open "list#[0]") (list.equivalence n.equivalence)] - (and (bit#= (at n.equivalence = left right) - (/.a/an = left right)) - (list#= (at list.functor each ++ (enum.range n.enum start end)) - (/.a/an each ++ (enum.range n.enum start end))))) - - second_order! - (/.a/an = - (enum.range n.enum start end) - (enum.range n.enum start end)) - - third_order! - (let [lln (/.a/an each (enum.range n.enum start) - (enum.range n.enum start end))] - (/.a/an = lln lln))] - (and first_order! - second_order! - third_order!))) - (_.coverage [/.with] - (/.with [n.addition] - (n.= (at n.addition composite left right) - (/.a/an composite left right)))) - (_.coverage [/.implicitly] - (n.= (at n.multiplication composite left right) - (/.a/an composite left right))) - )))) diff --git a/stdlib/source/test/lux/type/primitive.lux b/stdlib/source/test/lux/type/primitive.lux deleted file mode 100644 index 7b4500c00..000000000 --- a/stdlib/source/test/lux/type/primitive.lux +++ /dev/null @@ -1,89 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - ["[0]" meta] - [abstract - [monad (.only do)]] - [control - ["[0]" try] - ["[0]" exception]] - [data - ["[0]" text (.use "[1]#[0]" equivalence)]] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["[0]" template] - ["[0]" code (.only) - ["<[1]>" \\parser]]] - ["[0]" math (.only) - ["[0]" random] - [number - ["n" nat]]]]] - [\\library - ["[0]" /]]) - -(template.with_locals [g!Foo g!Bar] - (these (with_template [ ] - [(def - (syntax (_ []) - (do meta.monad - [frame ] - (in (list (code.text (the /.#name frame)))))))] - - [current /.current] - [specific (/.specific (template.text [g!Foo]))] - ) - - (/.primitive (g!Foo a) - Text - - (/.primitive (g!Bar a) - Nat - - (def .public test - Test - (<| (_.covering /._) - (_.for [/.primitive]) - (do random.monad - [expected_foo (random.lower_case 5) - expected_bar random.nat] - (all _.and - (_.coverage [/.abstraction] - (and (exec (is (g!Foo Text) - (/.abstraction g!Foo expected_foo)) - true) - (exec (is (g!Bar Text) - (/.abstraction expected_bar)) - true))) - (_.coverage [/.representation] - (and (|> expected_foo - (/.abstraction g!Foo) - (is (g!Foo Bit)) - (/.representation g!Foo) - (text#= expected_foo)) - (|> (/.abstraction expected_bar) - (is (g!Bar Bit)) - /.representation - (n.= expected_bar)))) - (_.coverage [/.transmutation] - (and (exec (|> expected_foo - (/.abstraction g!Foo) - (is (g!Foo .Macro)) - (/.transmutation g!Foo) - (is (g!Foo .Lux))) - true) - (exec (|> (/.abstraction expected_bar) - (is (g!Bar .Macro)) - /.transmutation - (is (g!Bar .Lux))) - true))) - (_.for [/.Frame] - (all _.and - (_.coverage [/.current] - (text#= (template.text [g!Bar]) - (..current))) - (_.coverage [/.specific] - (text#= (template.text [g!Foo]) - (..specific))) - )) - )))))))) diff --git a/stdlib/source/test/lux/type/quotient.lux b/stdlib/source/test/lux/type/quotient.lux deleted file mode 100644 index 72d39b19d..000000000 --- a/stdlib/source/test/lux/type/quotient.lux +++ /dev/null @@ -1,60 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - [abstract - ["[0]" monad (.only do)] - [\\specification - ["$[0]" equivalence]]] - [data - ["[0]" text (.use "[1]#[0]" equivalence) - ["%" \\format (.only format)]]] - [math - ["[0]" random (.only Random)] - [number - ["n" nat (.use "[1]#[0]" equivalence)]]]]] - [\\library - ["[0]" /]]) - -(def .public (random class super) - (All (_ t c %) (-> (/.Class t c %) (Random t) (Random (/.Quotient t c %)))) - (at random.monad each (/.quotient class) super)) - -(def mod_10_class - (/.class (|>> (n.% 10) %.nat))) - -(def Mod_10 - (/.type ..mod_10_class)) - -(def .public test - Test - (<| (_.covering /._) - (do random.monad - [modulus (random.only (n.> 0) random.nat) - .let [class (is (-> Nat Text) - (|>> (n.% modulus) %.nat))] - value random.nat] - (all _.and - (_.for [/.equivalence] - ($equivalence.spec (/.equivalence text.equivalence) - (..random (/.class class) random.nat))) - - (_.for [/.Class] - (_.coverage [/.class] - (same? (is Any class) - (is Any (/.class class))))) - (_.for [/.Quotient] - (all _.and - (_.coverage [/.quotient /.value /.label] - (let [quotient (/.quotient (/.class class) value)] - (and (same? value - (/.value quotient)) - (text#= (class value) - (/.label quotient))))) - (_.coverage [/.type] - (exec - (is ..Mod_10 - (/.quotient ..mod_10_class value)) - true)) - )) - )))) diff --git a/stdlib/source/test/lux/type/refinement.lux b/stdlib/source/test/lux/type/refinement.lux deleted file mode 100644 index 711d0401f..000000000 --- a/stdlib/source/test/lux/type/refinement.lux +++ /dev/null @@ -1,91 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - [abstract - [monad (.only do)]] - [control - ["[0]" maybe (.use "[1]#[0]" monad)] - [function - [predicate (.only Predicate)]]] - [data - [collection - ["[0]" list (.use "[1]#[0]" functor)]]] - [math - ["[0]" random] - [number - ["n" nat]]]]] - [\\library - ["[0]" /]]) - -(def _refiner - (/.refiner (n.> 123))) - -(def _type - (/.type _refiner)) - -(def .public test - Test - (<| (_.covering /._) - (_.for [/.Refined]) - (do [! random.monad] - [raw random.nat - modulus (at ! each (|>> (n.% 10) (n.+ 2)) random.nat) - .let [predicate (is (Predicate Nat) - (|>> (n.% modulus) (n.= 0)))] - total_raws (at ! each (|>> (n.% 20) ++) random.nat) - raws (random.list total_raws random.nat)] - (all _.and - (_.for [/.Refiner] - (all _.and - (_.coverage [/.refiner] - (case (/.refiner predicate raw) - {.#Some refined} - (predicate raw) - - {.#None} - (not (predicate raw)))) - (_.coverage [/.predicate] - (|> (/.refiner predicate modulus) - (maybe#each (|>> /.predicate (same? predicate))) - (maybe.else false))) - )) - (_.coverage [/.value] - (|> (/.refiner predicate modulus) - (maybe#each (|>> /.value (n.= modulus))) - (maybe.else false))) - (_.coverage [/.lifted] - (and (|> (/.refiner predicate modulus) - (maybe#each (/.lifted (n.+ modulus))) - maybe#conjoint - (maybe#each (|>> /.value (n.= (n.+ modulus modulus)))) - (maybe.else false)) - (|> (/.refiner predicate modulus) - (maybe#each (/.lifted (n.+ (++ modulus)))) - maybe#conjoint - (maybe#each (|>> /.value (n.= (n.+ modulus (++ modulus))))) - (maybe.else false) - not))) - (_.coverage [/.only] - (let [expected (list.only predicate raws) - actual (/.only (/.refiner predicate) raws)] - (and (n.= (list.size expected) - (list.size actual)) - (at (list.equivalence n.equivalence) = - expected - (list#each /.value actual))))) - (_.coverage [/.partition] - (let [expected (list.only predicate raws) - [actual alternative] (/.partition (/.refiner predicate) raws)] - (and (n.= (list.size expected) - (list.size actual)) - (n.= (n.- (list.size expected) total_raws) - (list.size alternative)) - (at (list.equivalence n.equivalence) = - expected - (list#each /.value actual))))) - (_.coverage [/.type] - (exec (is (Maybe .._type) - (.._refiner raw)) - true)) - )))) diff --git a/stdlib/source/test/lux/type/resource.lux b/stdlib/source/test/lux/type/resource.lux deleted file mode 100644 index a23f1cacf..000000000 --- a/stdlib/source/test/lux/type/resource.lux +++ /dev/null @@ -1,191 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - ["[0]" meta] - [abstract - ["[0]" monad (.only) - [indexed (.only do)]]] - [control - ["[0]" io (.only IO)] - ["[0]" try] - ["[0]" exception (.only Exception)] - [concurrency - ["[0]" async (.only Async)]]] - [data - ["[0]" identity (.only Identity)] - ["[0]" text (.use "[1]#[0]" equivalence) - ["%" \\format (.only format)]]] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["[0]" code (.only) - ["<[1]>" \\parser]]] - [math - ["[0]" random]]]] - [\\library - ["[0]" / (.only Res)]]) - -(def pure - Test - (monad.do [! random.monad] - [pre (at ! each %.nat random.nat) - post (at ! each %.nat random.nat) - .let [! identity.monad]] - (_.for [/.Linear /.run! /.monad] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage - (<| (text#= (format pre post)) - (is (Identity Text)) - (/.run! !) - (do (/.monad !) - - (in (format left right)))))] - - [[/.Affine /.Key /.Res /.Ordered /.ordered - /.Relevant /.read] - [res|left (/.ordered ! pre) - res|right (/.ordered ! post) - right (/.read ! res|right) - left (/.read ! res|left)]] - [[/.Commutative /.commutative /.exchange] - [res|left (/.commutative ! pre) - res|right (/.commutative ! post) - _ ((/.exchange [1 0]) !) - left (/.read ! res|left) - right (/.read ! res|right)]] - [[/.group /.un_group] - [res|left (/.commutative ! pre) - res|right (/.commutative ! post) - _ ((/.group 2) !) - _ ((/.un_group 2) !) - right (/.read ! res|right) - left (/.read ! res|left)]] - [[/.lifted] - [left (/.lifted ! pre) - right (/.lifted ! post)]] - )) - ))))) - -(def sync - Test - (monad.do [! random.monad] - [pre (at ! each %.nat random.nat) - post (at ! each %.nat random.nat) - .let [! io.monad]] - (_.for [/.Linear /.run! /.monad] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage - (<| (text#= (format pre post)) - io.run! - (is (IO Text)) - (/.run! !) - (do (/.monad !) - - (in (format left right)))))] - - [[/.Affine /.Key /.Res /.Ordered /.ordered - /.Relevant /.read] - [res|left (/.ordered ! pre) - res|right (/.ordered ! post) - right (/.read ! res|right) - left (/.read ! res|left)]] - [[/.Commutative /.commutative /.exchange] - [res|left (/.commutative ! pre) - res|right (/.commutative ! post) - _ ((/.exchange [1 0]) !) - left (/.read ! res|left) - right (/.read ! res|right)]] - [[/.group /.un_group] - [res|left (/.commutative ! pre) - res|right (/.commutative ! post) - _ ((/.group 2) !) - _ ((/.un_group 2) !) - right (/.read ! res|right) - left (/.read ! res|left)]] - [[/.lifted] - [left (/.lifted ! (io.io pre)) - right (/.lifted ! (io.io post))]] - )) - ))))) - -(def async - Test - (monad.do [! random.monad] - [pre (at ! each %.nat random.nat) - post (at ! each %.nat random.nat) - .let [! async.monad]] - (_.for [/.Linear /.run! /.monad] - (`` (all _.and - (~~ (with_template [ ] - [(in (monad.do ! - [outcome (<| (is (Async Text)) - (/.run! !) - (do (/.monad !) - - (in (format left right))))] - (_.coverage' - (text#= (format pre post) - outcome))))] - - [[/.Affine /.Key /.Res /.Ordered /.ordered - /.Relevant /.read] - [res|left (/.ordered ! pre) - res|right (/.ordered ! post) - right (/.read ! res|right) - left (/.read ! res|left)]] - [[/.Commutative /.commutative /.exchange] - [res|left (/.commutative ! pre) - res|right (/.commutative ! post) - _ ((/.exchange [1 0]) !) - left (/.read ! res|left) - right (/.read ! res|right)]] - [[/.group /.un_group] - [res|left (/.commutative ! pre) - res|right (/.commutative ! post) - _ ((/.group 2) !) - _ ((/.un_group 2) !) - right (/.read ! res|right) - left (/.read ! res|left)]] - [[/.lifted] - [left (/.lifted ! (async.resolved pre)) - right (/.lifted ! (async.resolved post))]] - )) - ))))) - -(def with_error - (syntax (_ [exception .symbol - to_expand .any]) - (monad.do meta.monad - [[_ _ exception] (meta.export exception)] - (function (_ compiler) - {.#Right [compiler - (list (code.bit (case ((macro.single_expansion to_expand) compiler) - {try.#Success _} - false - - {try.#Failure error} - true)))]})))) - -(def .public test - Test - (<| (_.covering /._) - (_.for [/.Procedure]) - (all _.and - ..pure - ..sync - ..async - - (_.coverage [/.amount_cannot_be_zero] - (`` (and (~~ (with_template [] - [(with_error /.amount_cannot_be_zero - ( 0))] - - [/.group] - [/.un_group] - ))))) - (_.coverage [/.index_cannot_be_repeated] - (with_error /.index_cannot_be_repeated - (/.exchange [0 0]))) - ))) diff --git a/stdlib/source/test/lux/type/unit.lux b/stdlib/source/test/lux/type/unit.lux deleted file mode 100644 index b52ddd921..000000000 --- a/stdlib/source/test/lux/type/unit.lux +++ /dev/null @@ -1,118 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - [abstract - [monad (.only do)] - [equivalence (.only Equivalence)] - [\\specification - ["$[0]" equivalence] - ["$[0]" order] - ["$[0]" enum]]] - [math - ["[0]" random (.only Random)] - [number - ["i" int]]]]] - [\\library - ["[0]" /]] - ["[0]" / - ["[1][0]" scale]]) - -(with_template [ ] - [(def ( range) - (-> Nat (Random (/.Measure Any ))) - (|> random.int - (at random.monad each (i.% (.int range))) - (random.only (|>> (i.= +0) not)) - (at random.monad each (at in))))] - - [meter /.Meter /.meter] - [second /.Second /.second] - ) - -(def polymorphism - Test - (all _.and - (_.for [/.equivalence] - ($equivalence.spec /.equivalence (..meter 1,000))) - (_.for [/.order] - ($order.spec /.order (..meter 1,000))) - (_.for [/.enum] - ($enum.spec /.enum (..meter 1,000))) - )) - -(def what (/.unit [])) -(def What (/.type what)) - -(def unit - Test - (do random.monad - [expected random.int] - (_.for [/.Unit] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage [ ] - (|> expected - (at in) - (at out) - (i.= expected)))] - - [/.Gram /.gram] - [/.Meter /.meter] - [/.Litre /.litre] - [/.Second /.second] - )) - (_.coverage [/.measure /.number] - (|> expected - /.measure - /.number - (i.= expected))) - (_.coverage [/.unit /.type] - (|> expected - (at ..what in) - (is (/.Measure Any What)) - (at ..what out) - (i.= expected))) - ))))) - -(def arithmetic - Test - (do random.monad - [.let [zero (at /.meter in +0) - (open "meter#[0]") (is (Equivalence (/.Measure Any /.Meter)) - /.equivalence)] - left (random.only (|>> (meter#= zero) not) (..meter 1,000)) - right (..meter 1,000) - extra (..second 1,000)] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage [] - (i.= ( (at /.meter out left) (at /.meter out right)) - (at /.meter out ( left right))))] - - [/.+ i.+] - [/.- i.-] - )) - (_.coverage [/.*] - (let [expected (i.* (at /.meter out left) (at /.meter out right)) - actual (/.number (is (/.Measure Any [/.Meter /.Meter]) - (/.* left right)))] - (i.= expected actual))) - (_.coverage [/./] - (|> right - (/.* left) - (/./ left) - (meter#= right))) - )))) - -(def .public test - Test - (<| (_.covering /._) - (_.for [/.Measure]) - (all _.and - ..polymorphism - ..unit - ..arithmetic - - /scale.test - ))) diff --git a/stdlib/source/test/lux/type/unit/scale.lux b/stdlib/source/test/lux/type/unit/scale.lux deleted file mode 100644 index adc3523b5..000000000 --- a/stdlib/source/test/lux/type/unit/scale.lux +++ /dev/null @@ -1,97 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - ["[0]" meta] - [abstract - [monad (.only do)] - [equivalence (.only Equivalence)]] - [macro - [syntax (.only syntax)] - ["[0]" code]] - [math - ["[0]" random (.only Random)] - [number - ["i" int] - ["[0]" ratio (.use "[1]#[0]" equivalence)]]]]] - [\\library - ["[0]" / (.only) - ["/[1]" //]]]) - -(def natural - (syntax (_ []) - (at meta.monad each - (|>> code.nat list) - meta.seed))) - -(with_expansions [ (..natural) - (..natural)] - (def how (/.scale [ratio.#denominator ratio.#numerator ])) - (def How (/.type how)) - - (def how::from ) - (def how::to ) - ) - -(def .public test - Test - (<| (_.covering /._) - (_.for [/.Scale]) - (do [! random.monad] - [small (|> random.int - (at ! each (i.% +1,000)) - (at ! each (at //.meter in))) - large (|> random.int - (at ! each (i.% +1,000)) - (at ! each (i.* +1,000,000,000)) - (at ! each (at //.meter in))) - .let [(open "meter#[0]") (is (Equivalence (//.Measure Any //.Meter)) - //.equivalence)] - unscaled (|> random.int - (at ! each (i.% +1,000)) - (at ! each (i.* (.int how::to))) - (at ! each (at //.meter in)))] - (`` (all _.and - (~~ (with_template [ ] - [(_.coverage [ ] - (|> small - (at up) - (is (//.Measure //.Meter)) - (at down) - (is (//.Measure Any //.Meter)) - (meter#= small)))] - - [/.Kilo /.kilo] - [/.Mega /.mega] - [/.Giga /.giga] - )) - (~~ (with_template [ ] - [(_.coverage [ ] - (|> large - (at up) - (is (//.Measure //.Meter)) - (at down) - (is (//.Measure Any //.Meter)) - (meter#= large)))] - - [/.Milli /.milli] - [/.Micro /.micro] - [/.Nano /.nano] - )) - (_.coverage [/.re_scaled] - (|> large (is (//.Measure Any //.Meter)) - (at /.kilo up) (is (//.Measure /.Kilo //.Meter)) - (/.re_scaled /.kilo /.milli) (is (//.Measure /.Milli //.Meter)) - (/.re_scaled /.milli /.kilo) (is (//.Measure /.Kilo //.Meter)) - (at /.kilo down) (is (//.Measure Any //.Meter)) - (meter#= large))) - (_.coverage [/.scale /.type] - (and (|> unscaled - (at ..how up) - (is (//.Measure How //.Meter)) - (at ..how down) - (meter#= unscaled)) - (ratio#= [ratio.#denominator ..how::from - ratio.#numerator ..how::to] - (at ..how ratio)))) - ))))) diff --git a/stdlib/source/test/lux/type/variance.lux b/stdlib/source/test/lux/type/variance.lux deleted file mode 100644 index 911c68067..000000000 --- a/stdlib/source/test/lux/type/variance.lux +++ /dev/null @@ -1,35 +0,0 @@ -(.require - [library - [lux (.except) - ["_" test (.only Test)] - [abstract - [monad (.only do)]] - [math - ["[0]" random (.only Random)]]]] - [\\library - ["[0]" / (.only) - ["/[1]" // (.only) - ["[1][0]" check]]]]) - -(type Super - (Ex (_ sub) [Text sub])) - -(type Sub - (Super Bit)) - -(def .public test - Test - (<| (_.covering /._) - (all _.and - (_.coverage [/.Co] - (and (//check.subsumes? (type_literal (/.Co Super)) (type_literal (/.Co Sub))) - (not (//check.subsumes? (type_literal (/.Co Sub)) (type_literal (/.Co Super)))))) - (_.coverage [/.Contra] - (and (//check.subsumes? (type_literal (/.Contra Sub)) (type_literal (/.Contra Super))) - (not (//check.subsumes? (type_literal (/.Contra Super)) (type_literal (/.Contra Sub)))))) - (_.coverage [/.In] - (and (//check.subsumes? (type_literal (/.In Super)) (type_literal (/.In Super))) - (//check.subsumes? (type_literal (/.In Sub)) (type_literal (/.In Sub))) - (not (//check.subsumes? (type_literal (/.In Sub)) (type_literal (/.In Super)))) - (not (//check.subsumes? (type_literal (/.In Super)) (type_literal (/.In Sub)))))) - ))) diff --git a/stdlib/source/test/lux/world/file/watch.lux b/stdlib/source/test/lux/world/file/watch.lux index 36f1f444b..6179b2164 100644 --- a/stdlib/source/test/lux/world/file/watch.lux +++ b/stdlib/source/test/lux/world/file/watch.lux @@ -55,8 +55,8 @@ ..concern) .let [[left left?] left [right right?] right]] - (_.coverage [/.also] - (let [composition (/.also left right)] + (_.coverage [/.and] + (let [composition (/.and left right)] (and (left? composition) (right? composition))))) (_.coverage [/.all] -- cgit v1.2.3