From 53ccae1625d46cf57247b9fb1cb9f4c28b0a0ad4 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 15 Nov 2017 22:04:44 -0400 Subject: - Moved "/type" and "/type/check" from "lux/meta" to "lux/lang". --- stdlib/test/test/lux/lang/type.lux | 165 +++++++++++++++++ stdlib/test/test/lux/lang/type/check.lux | 264 ++++++++++++++++++++++++++++ stdlib/test/test/lux/meta/type.lux | 165 ----------------- stdlib/test/test/lux/meta/type/check.lux | 264 ---------------------------- stdlib/test/test/lux/meta/type/implicit.lux | 19 +- stdlib/test/tests.lux | 8 +- 6 files changed, 441 insertions(+), 444 deletions(-) create mode 100644 stdlib/test/test/lux/lang/type.lux create mode 100644 stdlib/test/test/lux/lang/type/check.lux delete mode 100644 stdlib/test/test/lux/meta/type.lux delete mode 100644 stdlib/test/test/lux/meta/type/check.lux (limited to 'stdlib/test') diff --git a/stdlib/test/test/lux/lang/type.lux b/stdlib/test/test/lux/lang/type.lux new file mode 100644 index 000000000..a592df312 --- /dev/null +++ b/stdlib/test/test/lux/lang/type.lux @@ -0,0 +1,165 @@ +(;module: + lux + (lux [io] + (control ["M" monad #+ do Monad] + pipe) + (data [text "Text/" Monoid] + text/format + [number] + [maybe] + (coll [list])) + ["r" math/random] + (lang ["&" type])) + lux/test) + +## [Utils] +(def: gen-name + (r;Random Text) + (do r;Monad + [size (|> r;nat (:: @ map (n.% +10)))] + (r;text size))) + +(def: gen-ident + (r;Random Ident) + (r;seq gen-name gen-name)) + +(def: gen-type + (r;Random Type) + (let [(^open "R/") r;Monad] + (r;rec (function [gen-type] + ($_ r;alt + (r;seq gen-name (R/wrap (list))) + (R/wrap []) + (R/wrap []) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + r;nat + r;nat + r;nat + (r;seq (R/wrap (list)) gen-type) + (r;seq (R/wrap (list)) gen-type) + (r;seq gen-type gen-type) + (r;seq gen-ident gen-type) + ))))) + +## [Tests] +(context: "Types" + (<| (times +100) + (do @ + [sample gen-type] + (test "Every type is equal to itself." + (:: &;Eq = sample sample))))) + +(context: "Type application" + (test "Can apply quantified types (universal and existential quantification)." + (and (maybe;default false + (do maybe;Monad + [partial (&;apply (list Bool) Ann) + full (&;apply (list Int) partial)] + (wrap (:: &;Eq = full (#;Product Bool Int))))) + (|> (&;apply (list Bool) Text) + (case> #;None true _ false))))) + +(context: "Naming" + (let [base (#;Named ["" "a"] (#;Product Bool Int)) + aliased (#;Named ["" "c"] + (#;Named ["" "b"] + base))] + ($_ seq + (test "Can remove aliases from an already-named type." + (:: &;Eq = + base + (&;un-alias aliased))) + + (test "Can remove all names from a type." + (and (not (:: &;Eq = + base + (&;un-name aliased))) + (:: &;Eq = + (&;un-name base) + (&;un-name aliased))))))) + +(context: "Type construction [structs]" + (<| (times +100) + (do @ + [size (|> r;nat (:: @ map (n.% +3))) + members (|> gen-type + (r;filter (function [type] + (case type + (^or (#;Sum _) (#;Product _)) + false + + _ + true))) + (list;repeat size) + (M;seq @)) + #let [(^open "&/") &;Eq + (^open "L/") (list;Eq &;Eq)]] + (with-expansions + [ (do-template [ ] + [(test (format "Can build and tear-down " " types.") + (let [flat (|> members )] + (or (L/= members flat) + (and (L/= (list) members) + (L/= (list ) flat)))))] + + ["variant" &;variant &;flatten-variant Void] + ["tuple" &;tuple &;flatten-tuple Unit] + )] + ($_ seq + + ))))) + +(context: "Type construction [parameterized]" + (<| (times +100) + (do @ + [size (|> r;nat (:: @ map (n.% +3))) + members (M;seq @ (list;repeat size gen-type)) + extra (|> gen-type + (r;filter (function [type] + (case type + (^or (#;Function _) (#;Apply _)) + false + + _ + true)))) + #let [(^open "&/") &;Eq + (^open "L/") (list;Eq &;Eq)]] + ($_ seq + (test "Can build and tear-down function types." + (let [[inputs output] (|> (&;function members extra) &;flatten-function)] + (and (L/= members inputs) + (&/= extra output)))) + + (test "Can build and tear-down application types." + (let [[tfunc tparams] (|> extra (&;application members) &;flatten-application)] + (n.= (list;size members) (list;size tparams)))) + )))) + +(context: "Type construction [higher order]" + (<| (times +100) + (do @ + [size (|> r;nat (:: @ map (n.% +3))) + extra (|> gen-type + (r;filter (function [type] + (case type + (^or (#;UnivQ _) (#;ExQ _)) + false + + _ + true)))) + #let [(^open "&/") &;Eq]] + (with-expansions + [ (do-template [ ] + [(test (format "Can build and tear-down " " types.") + (let [[flat-size flat-body] (|> extra ( size) )] + (and (n.= size flat-size) + (&/= extra flat-body))))] + + ["universally-quantified" &;univ-q &;flatten-univ-q] + ["existentially-quantified" &;ex-q &;flatten-ex-q] + )] + ($_ seq + + ))))) diff --git a/stdlib/test/test/lux/lang/type/check.lux b/stdlib/test/test/lux/lang/type/check.lux new file mode 100644 index 000000000..32f7e832b --- /dev/null +++ b/stdlib/test/test/lux/lang/type/check.lux @@ -0,0 +1,264 @@ +(;module: + lux + (lux [io] + (control [monad #+ do Monad] + [pipe #+ case>]) + (data [product] + [maybe] + [number] + [text "text/" Monoid Eq] + text/format + (coll [list "list/" Functor] + [set])) + ["r" math/random] + (lang [type "type/" Eq] + ["@" type/check])) + lux/test) + +## [Utils] +(def: gen-name + (r;Random Text) + (do r;Monad + [size (|> r;nat (:: @ map (n.% +10)))] + (r;text size))) + +(def: gen-ident + (r;Random Ident) + (r;seq gen-name gen-name)) + +(def: gen-type + (r;Random Type) + (let [(^open "r/") r;Monad] + (r;rec (function [gen-type] + ($_ r;alt + (r;seq gen-name (r/wrap (list))) + (r/wrap []) + (r/wrap []) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + (r;seq gen-type gen-type) + r;nat + r;nat + r;nat + (r;seq (r/wrap (list)) gen-type) + (r;seq (r/wrap (list)) gen-type) + (r;seq gen-type gen-type) + (r;seq gen-ident gen-type) + ))))) + +(def: (valid-type? type) + (-> Type Bool) + (case type + (#;Primitive name params) + (list;every? valid-type? params) + + (^or #;Void #;Unit (#;Ex id)) + true + + (^template [] + ( left right) + (and (valid-type? left) (valid-type? right))) + ([#;Sum] [#;Product] [#;Function]) + + (#;Named name type') + (valid-type? type') + + _ + false)) + +(def: (type-checks? input) + (-> (@;Check []) Bool) + (case (@;run @;fresh-context input) + (#;Right []) + true + + (#;Left error) + false)) + +## [Tests] +(context: "Top and Bottom." + (<| (times +100) + (do @ + [sample (|> gen-type (r;filter valid-type?))] + ($_ seq + (test "Top is the super-type of everything." + (@;checks? Top sample)) + + (test "Bottom is the sub-type of everything." + (@;checks? sample Bottom)) + )))) + +(context: "Simple type-checking." + ($_ seq + (test "Unit and Void match themselves." + (and (@;checks? Void Void) + (@;checks? Unit Unit))) + + (test "Existential types only match with themselves." + (and (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check exT exT))) + (not (type-checks? (do @;Monad + [[_ exTL] @;existential + [_ exTR] @;existential] + (@;check exTL exTR)))))) + + (test "Names do not affect type-checking." + (and (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + exT))) + (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check exT + (#;Named ["module" "name"] exT)))) + (type-checks? (do @;Monad + [[_ exT] @;existential] + (@;check (#;Named ["module" "name"] exT) + (#;Named ["module" "name"] exT)))))) + + (test "Functions are covariant on inputs and contravariant on outputs." + (and (@;checks? (#;Function Bottom Top) + (#;Function Top Bottom)) + (not (@;checks? (#;Function Top Bottom) + (#;Function Bottom Top))))) + )) + +(context: "Type application." + (<| (times +100) + (do @ + [meta gen-type + data gen-type] + (test "Can type-check type application." + (and (@;checks? (|> Ann (#;Apply meta) (#;Apply data)) + (type;tuple (list meta data))) + (@;checks? (type;tuple (list meta data)) + (|> Ann (#;Apply meta) (#;Apply data)))))))) + +(context: "Primitive types." + (<| (times +100) + (do @ + [nameL gen-name + nameR (|> gen-name (r;filter (. not (text/= nameL)))) + paramL gen-type + paramR (|> gen-type (r;filter (|>. (@;checks? paramL) not)))] + ($_ seq + (test "Primitive types match when they have the same name and the same parameters." + (@;checks? (#;Primitive nameL (list paramL)) + (#;Primitive nameL (list paramL)))) + + (test "Names matter to primitive types." + (not (@;checks? (#;Primitive nameL (list paramL)) + (#;Primitive nameR (list paramL))))) + + (test "Parameters matter to primitive types." + (not (@;checks? (#;Primitive nameL (list paramL)) + (#;Primitive nameL (list paramR))))) + )))) + +(context: "Type variables." + ($_ seq + (test "Type-vars check against themselves." + (type-checks? (do @;Monad + [[id var] @;var] + (@;check var var)))) + + (test "Can bind unbound type-vars by type-checking against them." + (and (type-checks? (do @;Monad + [[id var] @;var] + (@;check var #;Unit))) + (type-checks? (do @;Monad + [[id var] @;var] + (@;check #;Unit var))))) + + (test "Cannot rebind already bound type-vars." + (not (type-checks? (do @;Monad + [[id var] @;var + _ (@;check var #;Unit)] + (@;check var #;Void))))) + + (test "If the type bound to a var is a super-type to another, then the var is also a super-type." + (type-checks? (do @;Monad + [[id var] @;var + _ (@;check var Top)] + (@;check var #;Unit)))) + + (test "If the type bound to a var is a sub-type of another, then the var is also a sub-type." + (type-checks? (do @;Monad + [[id var] @;var + _ (@;check var Bottom)] + (@;check #;Unit var)))) + )) + +(def: (build-ring num-connections) + (-> Nat (@;Check [[Nat Type] (List [Nat Type]) [Nat Type]])) + (do @;Monad + [[head-id head-type] @;var + ids+types (monad;seq @ (list;repeat num-connections @;var)) + [tail-id tail-type] (monad;fold @ (function [[tail-id tail-type] [_head-id _head-type]] + (do @ + [_ (@;check head-type tail-type)] + (wrap [tail-id tail-type]))) + [head-id head-type] + ids+types)] + (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) + +(context: "Rings of type variables." + (<| (times +100) + (do @ + [num-connections (|> r;nat (:: @ map (n.% +100))) + boundT (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) + pick-pcg (r;seq r;nat r;nat)] + ($_ seq + (test "Can create rings of variables." + (type-checks? (do @;Monad + [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections) + #let [ids (list/map product;left ids+types)] + headR (@;ring head-id) + tailR (@;ring tail-id)] + (@;assert "" + (let [same-rings? (:: set;Eq = headR tailR) + expected-size? (n.= (n.inc num-connections) (set;size headR)) + same-vars? (|> (set;to-list headR) + (list;sort n.<) + (:: (list;Eq number;Eq) = (list;sort n.< (#;Cons head-id ids))))] + (and same-rings? + expected-size? + same-vars?)))))) + (test "When a var in a ring is bound, all the ring is bound." + (type-checks? (do @;Monad + [[[head-id headT] ids+types tailT] (build-ring num-connections) + #let [ids (list/map product;left ids+types)] + _ (@;check headT boundT) + head-bound (@;read head-id) + tail-bound (monad;map @ @;read ids) + headR (@;ring head-id) + tailR+ (monad;map @ @;ring ids)] + (let [rings-were-erased? (and (set;empty? headR) + (list;every? set;empty? tailR+)) + same-types? (list;every? (type/= boundT) (list& (maybe;default headT head-bound) + (list/map (function [[tail-id ?tailT]] + (maybe;default (#;Var tail-id) ?tailT)) + (list;zip2 ids tail-bound))))] + (@;assert "" + (and rings-were-erased? + same-types?)))))) + (test "Can merge multiple rings of variables." + (type-checks? (do @;Monad + [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections) + [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections) + headRL-pre (@;ring head-idL) + headRR-pre (@;ring head-idR) + _ (@;check headTL headTR) + headRL-post (@;ring head-idL) + headRR-post (@;ring head-idR)] + (@;assert "" + (let [same-rings? (:: set;Eq = headRL-post headRR-post) + expected-size? (n.= (n.* +2 (n.inc num-connections)) + (set;size headRL-post)) + union? (:: set;Eq = headRL-post (set;union headRL-pre headRR-pre))] + (and same-rings? + expected-size? + union?)))))) + )) + )) diff --git a/stdlib/test/test/lux/meta/type.lux b/stdlib/test/test/lux/meta/type.lux deleted file mode 100644 index abddcc033..000000000 --- a/stdlib/test/test/lux/meta/type.lux +++ /dev/null @@ -1,165 +0,0 @@ -(;module: - lux - (lux [io] - (control ["M" monad #+ do Monad] - pipe) - (data [text "Text/" Monoid] - text/format - [number] - [maybe] - (coll [list])) - ["r" math/random] - (meta ["&" type])) - lux/test) - -## [Utils] -(def: gen-name - (r;Random Text) - (do r;Monad - [size (|> r;nat (:: @ map (n.% +10)))] - (r;text size))) - -(def: gen-ident - (r;Random Ident) - (r;seq gen-name gen-name)) - -(def: gen-type - (r;Random Type) - (let [(^open "R/") r;Monad] - (r;rec (function [gen-type] - ($_ r;alt - (r;seq gen-name (R/wrap (list))) - (R/wrap []) - (R/wrap []) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - r;nat - r;nat - r;nat - (r;seq (R/wrap (list)) gen-type) - (r;seq (R/wrap (list)) gen-type) - (r;seq gen-type gen-type) - (r;seq gen-ident gen-type) - ))))) - -## [Tests] -(context: "Types" - (<| (times +100) - (do @ - [sample gen-type] - (test "Every type is equal to itself." - (:: &;Eq = sample sample))))) - -(context: "Type application" - (test "Can apply quantified types (universal and existential quantification)." - (and (maybe;default false - (do maybe;Monad - [partial (&;apply (list Bool) Ann) - full (&;apply (list Int) partial)] - (wrap (:: &;Eq = full (#;Product Bool Int))))) - (|> (&;apply (list Bool) Text) - (case> #;None true _ false))))) - -(context: "Naming" - (let [base (#;Named ["" "a"] (#;Product Bool Int)) - aliased (#;Named ["" "c"] - (#;Named ["" "b"] - base))] - ($_ seq - (test "Can remove aliases from an already-named type." - (:: &;Eq = - base - (&;un-alias aliased))) - - (test "Can remove all names from a type." - (and (not (:: &;Eq = - base - (&;un-name aliased))) - (:: &;Eq = - (&;un-name base) - (&;un-name aliased))))))) - -(context: "Type construction [structs]" - (<| (times +100) - (do @ - [size (|> r;nat (:: @ map (n.% +3))) - members (|> gen-type - (r;filter (function [type] - (case type - (^or (#;Sum _) (#;Product _)) - false - - _ - true))) - (list;repeat size) - (M;seq @)) - #let [(^open "&/") &;Eq - (^open "L/") (list;Eq &;Eq)]] - (with-expansions - [ (do-template [ ] - [(test (format "Can build and tear-down " " types.") - (let [flat (|> members )] - (or (L/= members flat) - (and (L/= (list) members) - (L/= (list ) flat)))))] - - ["variant" &;variant &;flatten-variant Void] - ["tuple" &;tuple &;flatten-tuple Unit] - )] - ($_ seq - - ))))) - -(context: "Type construction [parameterized]" - (<| (times +100) - (do @ - [size (|> r;nat (:: @ map (n.% +3))) - members (M;seq @ (list;repeat size gen-type)) - extra (|> gen-type - (r;filter (function [type] - (case type - (^or (#;Function _) (#;Apply _)) - false - - _ - true)))) - #let [(^open "&/") &;Eq - (^open "L/") (list;Eq &;Eq)]] - ($_ seq - (test "Can build and tear-down function types." - (let [[inputs output] (|> (&;function members extra) &;flatten-function)] - (and (L/= members inputs) - (&/= extra output)))) - - (test "Can build and tear-down application types." - (let [[tfunc tparams] (|> extra (&;application members) &;flatten-application)] - (n.= (list;size members) (list;size tparams)))) - )))) - -(context: "Type construction [higher order]" - (<| (times +100) - (do @ - [size (|> r;nat (:: @ map (n.% +3))) - extra (|> gen-type - (r;filter (function [type] - (case type - (^or (#;UnivQ _) (#;ExQ _)) - false - - _ - true)))) - #let [(^open "&/") &;Eq]] - (with-expansions - [ (do-template [ ] - [(test (format "Can build and tear-down " " types.") - (let [[flat-size flat-body] (|> extra ( size) )] - (and (n.= size flat-size) - (&/= extra flat-body))))] - - ["universally-quantified" &;univ-q &;flatten-univ-q] - ["existentially-quantified" &;ex-q &;flatten-ex-q] - )] - ($_ seq - - ))))) diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux deleted file mode 100644 index 127e02cbd..000000000 --- a/stdlib/test/test/lux/meta/type/check.lux +++ /dev/null @@ -1,264 +0,0 @@ -(;module: - lux - (lux [io] - (control [monad #+ do Monad] - [pipe #+ case>]) - (data [product] - [maybe] - [number] - [text "text/" Monoid Eq] - text/format - (coll [list "list/" Functor] - [set])) - ["r" math/random] - (meta [type "type/" Eq] - ["@" type/check])) - lux/test) - -## [Utils] -(def: gen-name - (r;Random Text) - (do r;Monad - [size (|> r;nat (:: @ map (n.% +10)))] - (r;text size))) - -(def: gen-ident - (r;Random Ident) - (r;seq gen-name gen-name)) - -(def: gen-type - (r;Random Type) - (let [(^open "r/") r;Monad] - (r;rec (function [gen-type] - ($_ r;alt - (r;seq gen-name (r/wrap (list))) - (r/wrap []) - (r/wrap []) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - (r;seq gen-type gen-type) - r;nat - r;nat - r;nat - (r;seq (r/wrap (list)) gen-type) - (r;seq (r/wrap (list)) gen-type) - (r;seq gen-type gen-type) - (r;seq gen-ident gen-type) - ))))) - -(def: (valid-type? type) - (-> Type Bool) - (case type - (#;Primitive name params) - (list;every? valid-type? params) - - (^or #;Void #;Unit (#;Ex id)) - true - - (^template [] - ( left right) - (and (valid-type? left) (valid-type? right))) - ([#;Sum] [#;Product] [#;Function]) - - (#;Named name type') - (valid-type? type') - - _ - false)) - -(def: (type-checks? input) - (-> (@;Check []) Bool) - (case (@;run @;fresh-context input) - (#;Right []) - true - - (#;Left error) - false)) - -## [Tests] -(context: "Top and Bottom." - (<| (times +100) - (do @ - [sample (|> gen-type (r;filter valid-type?))] - ($_ seq - (test "Top is the super-type of everything." - (@;checks? Top sample)) - - (test "Bottom is the sub-type of everything." - (@;checks? sample Bottom)) - )))) - -(context: "Simple type-checking." - ($_ seq - (test "Unit and Void match themselves." - (and (@;checks? Void Void) - (@;checks? Unit Unit))) - - (test "Existential types only match with themselves." - (and (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check exT exT))) - (not (type-checks? (do @;Monad - [[_ exTL] @;existential - [_ exTR] @;existential] - (@;check exTL exTR)))))) - - (test "Names do not affect type-checking." - (and (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check (#;Named ["module" "name"] exT) - exT))) - (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check exT - (#;Named ["module" "name"] exT)))) - (type-checks? (do @;Monad - [[_ exT] @;existential] - (@;check (#;Named ["module" "name"] exT) - (#;Named ["module" "name"] exT)))))) - - (test "Functions are covariant on inputs and contravariant on outputs." - (and (@;checks? (#;Function Bottom Top) - (#;Function Top Bottom)) - (not (@;checks? (#;Function Top Bottom) - (#;Function Bottom Top))))) - )) - -(context: "Type application." - (<| (times +100) - (do @ - [meta gen-type - data gen-type] - (test "Can type-check type application." - (and (@;checks? (|> Ann (#;Apply meta) (#;Apply data)) - (type;tuple (list meta data))) - (@;checks? (type;tuple (list meta data)) - (|> Ann (#;Apply meta) (#;Apply data)))))))) - -(context: "Primitive types." - (<| (times +100) - (do @ - [nameL gen-name - nameR (|> gen-name (r;filter (. not (text/= nameL)))) - paramL gen-type - paramR (|> gen-type (r;filter (|>. (@;checks? paramL) not)))] - ($_ seq - (test "Primitive types match when they have the same name and the same parameters." - (@;checks? (#;Primitive nameL (list paramL)) - (#;Primitive nameL (list paramL)))) - - (test "Names matter to primitive types." - (not (@;checks? (#;Primitive nameL (list paramL)) - (#;Primitive nameR (list paramL))))) - - (test "Parameters matter to primitive types." - (not (@;checks? (#;Primitive nameL (list paramL)) - (#;Primitive nameL (list paramR))))) - )))) - -(context: "Type variables." - ($_ seq - (test "Type-vars check against themselves." - (type-checks? (do @;Monad - [[id var] @;var] - (@;check var var)))) - - (test "Can bind unbound type-vars by type-checking against them." - (and (type-checks? (do @;Monad - [[id var] @;var] - (@;check var #;Unit))) - (type-checks? (do @;Monad - [[id var] @;var] - (@;check #;Unit var))))) - - (test "Cannot rebind already bound type-vars." - (not (type-checks? (do @;Monad - [[id var] @;var - _ (@;check var #;Unit)] - (@;check var #;Void))))) - - (test "If the type bound to a var is a super-type to another, then the var is also a super-type." - (type-checks? (do @;Monad - [[id var] @;var - _ (@;check var Top)] - (@;check var #;Unit)))) - - (test "If the type bound to a var is a sub-type of another, then the var is also a sub-type." - (type-checks? (do @;Monad - [[id var] @;var - _ (@;check var Bottom)] - (@;check #;Unit var)))) - )) - -(def: (build-ring num-connections) - (-> Nat (@;Check [[Nat Type] (List [Nat Type]) [Nat Type]])) - (do @;Monad - [[head-id head-type] @;var - ids+types (monad;seq @ (list;repeat num-connections @;var)) - [tail-id tail-type] (monad;fold @ (function [[tail-id tail-type] [_head-id _head-type]] - (do @ - [_ (@;check head-type tail-type)] - (wrap [tail-id tail-type]))) - [head-id head-type] - ids+types)] - (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) - -(context: "Rings of type variables." - (<| (times +100) - (do @ - [num-connections (|> r;nat (:: @ map (n.% +100))) - boundT (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) - pick-pcg (r;seq r;nat r;nat)] - ($_ seq - (test "Can create rings of variables." - (type-checks? (do @;Monad - [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections) - #let [ids (list/map product;left ids+types)] - headR (@;ring head-id) - tailR (@;ring tail-id)] - (@;assert "" - (let [same-rings? (:: set;Eq = headR tailR) - expected-size? (n.= (n.inc num-connections) (set;size headR)) - same-vars? (|> (set;to-list headR) - (list;sort n.<) - (:: (list;Eq number;Eq) = (list;sort n.< (#;Cons head-id ids))))] - (and same-rings? - expected-size? - same-vars?)))))) - (test "When a var in a ring is bound, all the ring is bound." - (type-checks? (do @;Monad - [[[head-id headT] ids+types tailT] (build-ring num-connections) - #let [ids (list/map product;left ids+types)] - _ (@;check headT boundT) - head-bound (@;read head-id) - tail-bound (monad;map @ @;read ids) - headR (@;ring head-id) - tailR+ (monad;map @ @;ring ids)] - (let [rings-were-erased? (and (set;empty? headR) - (list;every? set;empty? tailR+)) - same-types? (list;every? (type/= boundT) (list& (maybe;default headT head-bound) - (list/map (function [[tail-id ?tailT]] - (maybe;default (#;Var tail-id) ?tailT)) - (list;zip2 ids tail-bound))))] - (@;assert "" - (and rings-were-erased? - same-types?)))))) - (test "Can merge multiple rings of variables." - (type-checks? (do @;Monad - [[[head-idL headTL] ids+typesL [tail-idL tailTL]] (build-ring num-connections) - [[head-idR headTR] ids+typesR [tail-idR tailTR]] (build-ring num-connections) - headRL-pre (@;ring head-idL) - headRR-pre (@;ring head-idR) - _ (@;check headTL headTR) - headRL-post (@;ring head-idL) - headRR-post (@;ring head-idR)] - (@;assert "" - (let [same-rings? (:: set;Eq = headRL-post headRR-post) - expected-size? (n.= (n.* +2 (n.inc num-connections)) - (set;size headRL-post)) - union? (:: set;Eq = headRL-post (set;union headRL-pre headRR-pre))] - (and same-rings? - expected-size? - union?)))))) - )) - )) diff --git a/stdlib/test/test/lux/meta/type/implicit.lux b/stdlib/test/test/lux/meta/type/implicit.lux index 8c05b01af..6d2344120 100644 --- a/stdlib/test/test/lux/meta/type/implicit.lux +++ b/stdlib/test/test/lux/meta/type/implicit.lux @@ -4,15 +4,12 @@ (control [monad #+ do Monad] functor [eq]) - (data [text "Text/" Monoid] - text/format - [number] - [bool "B/" Eq] + (data [number] + [bool "bool/" Eq] maybe (coll [list])) ["r" math/random] - (meta [type] - type/implicit)) + (meta type/implicit)) lux/test) (context: "Automatic structure selection" @@ -22,11 +19,11 @@ y r;nat] ($_ seq (test "Can automatically select first-order structures." - (let [(^open "L/") (list;Eq number;Eq)] - (and (B/= (:: number;Eq = x y) - (::: = x y)) - (L/= (list;n.range +1 +10) - (::: map n.inc (list;n.range +0 +9))) + (let [(^open "list/") (list;Eq number;Eq)] + (and (bool/= (:: number;Eq = x y) + (::: = x y)) + (list/= (list;n.range +1 +10) + (::: map n.inc (list;n.range +0 +9))) ))) (test "Can automatically select second-order structures." diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux index d4e038774..3e1d6b5f3 100644 --- a/stdlib/test/tests.lux +++ b/stdlib/test/tests.lux @@ -66,11 +66,11 @@ ["_;" syntax] (poly ["poly_;" eq] ["poly_;" functor]) - ["_;" type] - (type ["_;" check] - ["_;" implicit] + (type ["_;" implicit] ["_;" object])) - (lang ["lang_;" syntax]) + (lang ["lang_;" syntax] + ["_;" type] + (type ["_;" check])) (world ["_;" blob] ["_;" file] (net ["_;" tcp] -- cgit v1.2.3