From 360c8f0cd43452d4a47cdd2002625143b96df6c8 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 15 Nov 2017 21:05:59 -0400 Subject: - Re-named "lux/meta/type/auto" to "lux/meta/type/implicit". --- stdlib/source/lux/data/store.lux | 2 +- stdlib/source/lux/meta/type/auto.lux | 363 ---------------------------- stdlib/source/lux/meta/type/implicit.lux | 363 ++++++++++++++++++++++++++++ stdlib/test/test/lux/meta/type/auto.lux | 41 ---- stdlib/test/test/lux/meta/type/implicit.lux | 41 ++++ stdlib/test/tests.lux | 2 +- 6 files changed, 406 insertions(+), 406 deletions(-) delete mode 100644 stdlib/source/lux/meta/type/auto.lux create mode 100644 stdlib/source/lux/meta/type/implicit.lux delete mode 100644 stdlib/test/test/lux/meta/type/auto.lux create mode 100644 stdlib/test/test/lux/meta/type/implicit.lux diff --git a/stdlib/source/lux/data/store.lux b/stdlib/source/lux/data/store.lux index f798078dd..f2713c6b8 100644 --- a/stdlib/source/lux/data/store.lux +++ b/stdlib/source/lux/data/store.lux @@ -2,7 +2,7 @@ lux (lux (control ["F" functor] comonad) - (meta (type auto)))) + (meta (type implicit)))) (type: #export (Store s a) {#cursor s diff --git a/stdlib/source/lux/meta/type/auto.lux b/stdlib/source/lux/meta/type/auto.lux deleted file mode 100644 index a2013d3b1..000000000 --- a/stdlib/source/lux/meta/type/auto.lux +++ /dev/null @@ -1,363 +0,0 @@ -(;module: - lux - (lux (control ["M" monad #+ do Monad] - [eq] - ["p" parser]) - (data [text "Text/" Eq] - text/format - [number] - (coll [list "List/" Monad Fold] - [dict]) - [bool] - [product] - [maybe]) - [meta #+ Monad] - (meta [code] - ["s" syntax #+ syntax: Syntax] - [type] - (type ["tc" check #+ Check Monad])) - )) - -(def: (find-type-var id env) - (-> Nat Type-Context (Meta Type)) - (case (list;find (|>. product;left (n.= id)) - (get@ #;var-bindings env)) - (#;Some [_ (#;Some type)]) - (case type - (#;Var id') - (find-type-var id' env) - - _ - (:: Monad wrap type)) - - (#;Some [_ #;None]) - (meta;fail (format "Unbound type-var " (%n id))) - - #;None - (meta;fail (format "Unknown type-var " (%n id))) - )) - -(def: (resolve-type var-name) - (-> Ident (Meta Type)) - (do Monad - [raw-type (meta;find-type var-name) - compiler meta;get-compiler] - (case raw-type - (#;Var id) - (find-type-var id (get@ #;type-context compiler)) - - _ - (wrap raw-type)))) - -(def: (find-member-type idx sig-type) - (-> Nat Type (Check Type)) - (case sig-type - (#;Named _ sig-type') - (find-member-type idx sig-type') - - (#;Apply arg func) - (case (type;apply (list arg) func) - #;None - (tc;fail (format "Cannot apply type " (%type func) " to type " (%type arg))) - - (#;Some sig-type') - (find-member-type idx sig-type')) - - (#;Product left right) - (if (n.= +0 idx) - (:: Monad wrap left) - (find-member-type (n.dec idx) right)) - - _ - (if (n.= +0 idx) - (:: Monad wrap sig-type) - (tc;fail (format "Cannot find member type " (%n idx) " for " (%type sig-type)))))) - -(def: (find-member-name member) - (-> Ident (Meta Ident)) - (case member - ["" simple-name] - (meta;either (do Monad - [member (meta;normalize member) - _ (meta;resolve-tag member)] - (wrap member)) - (do Monad - [this-module-name meta;current-module-name - imp-mods (meta;imported-modules this-module-name) - tag-lists (M;map @ meta;tag-lists imp-mods) - #let [tag-lists (|> tag-lists List/join (List/map product;left) List/join) - candidates (list;filter (. (Text/= simple-name) product;right) - tag-lists)]] - (case candidates - #;Nil - (meta;fail (format "Unknown tag: " (%ident member))) - - (#;Cons winner #;Nil) - (wrap winner) - - _ - (meta;fail (format "Too many candidate tags: " (%list %ident candidates)))))) - - _ - (:: Monad wrap member))) - -(def: (resolve-member member) - (-> Ident (Meta [Nat Type])) - (do Monad - [member (find-member-name member) - [idx tag-list sig-type] (meta;resolve-tag member)] - (wrap [idx sig-type]))) - -(def: (prepare-defs this-module-name defs) - (-> Text (List [Text Def]) (List [Ident Type])) - (|> defs - (list;filter (function [[name [def-type def-anns def-value]]] - (meta;struct? def-anns))) - (List/map (function [[name [def-type def-anns def-value]]] - [[this-module-name name] def-type])))) - -(def: local-env - (Meta (List [Ident Type])) - (do Monad - [local-batches meta;locals - #let [total-locals (List/fold (function [[name type] table] - (dict;put~ name type table)) - (: (dict;Dict Text Type) - (dict;new text;Hash)) - (List/join local-batches))]] - (wrap (|> total-locals - dict;entries - (List/map (function [[name type]] [["" name] type])))))) - -(def: local-structs - (Meta (List [Ident Type])) - (do Monad - [this-module-name meta;current-module-name - defs (meta;defs this-module-name)] - (wrap (prepare-defs this-module-name defs)))) - -(def: import-structs - (Meta (List [Ident Type])) - (do Monad - [this-module-name meta;current-module-name - imp-mods (meta;imported-modules this-module-name) - export-batches (M;map @ (function [imp-mod] - (do @ - [exports (meta;exports imp-mod)] - (wrap (prepare-defs imp-mod exports)))) - imp-mods)] - (wrap (List/join export-batches)))) - -(def: (apply-function-type func arg) - (-> Type Type (Check Type)) - (case func - (#;Named _ func') - (apply-function-type func' arg) - - (#;UnivQ _) - (do Monad - [[id var] tc;var] - (apply-function-type (maybe;assume (type;apply (list var) func)) - arg)) - - (#;Function input output) - (do Monad - [_ (tc;check input arg)] - (wrap output)) - - _ - (tc;fail (format "Invalid function type: " (%type func))))) - -(def: (concrete-type type) - (-> Type (Check [(List Nat) Type])) - (case type - (#;UnivQ _) - (do Monad - [[id var] tc;var - [ids final-output] (concrete-type (maybe;assume (type;apply (list var) type)))] - (wrap [(#;Cons id ids) - final-output])) - - _ - (:: Monad wrap [(list) type]))) - -(def: (check-apply member-type input-types output-type) - (-> Type (List Type) Type (Check [])) - (do Monad - [member-type' (M;fold Monad - (function [input member] - (apply-function-type member input)) - member-type - input-types)] - (tc;check output-type member-type'))) - -(type: #rec Instance - {#constructor Ident - #dependencies (List Instance)}) - -(def: (test-provision provision context dep alts) - (-> (-> Compiler Type-Context Type (Check Instance)) - Type-Context Type (List [Ident Type]) - (Meta (List Instance))) - (do Monad - [compiler meta;get-compiler] - (case (|> alts - (List/map (function [[alt-name alt-type]] - (case (tc;run context - (do Monad - [[tvars alt-type] (concrete-type alt-type) - #let [[deps alt-type] (type;flatten-function alt-type)] - _ (tc;check dep alt-type) - context' tc;get-context - =deps (M;map @ (provision compiler context') deps)] - (wrap =deps))) - (#;Left error) - (list) - - (#;Right =deps) - (list [alt-name =deps])))) - List/join) - #;Nil - (meta;fail (format "No candidates for provisioning: " (%type dep))) - - found - (wrap found)))) - -(def: (provision compiler context dep) - (-> Compiler Type-Context Type (Check Instance)) - (case (meta;run compiler - ($_ meta;either - (do Monad [alts local-env] (test-provision provision context dep alts)) - (do Monad [alts local-structs] (test-provision provision context dep alts)) - (do Monad [alts import-structs] (test-provision provision context dep alts)))) - (#;Left error) - (tc;fail error) - - (#;Right candidates) - (case candidates - #;Nil - (tc;fail (format "No candidates for provisioning: " (%type dep))) - - (#;Cons winner #;Nil) - (:: Monad wrap winner) - - _ - (tc;fail (format "Too many candidates for provisioning: " (%type dep) " --- " (%list (. %ident product;left) candidates)))) - )) - -(def: (test-alternatives sig-type member-idx input-types output-type alts) - (-> Type Nat (List Type) Type (List [Ident Type]) (Meta (List Instance))) - (do Monad - [compiler meta;get-compiler - context meta;type-context] - (case (|> alts - (List/map (function [[alt-name alt-type]] - (case (tc;run context - (do Monad - [[tvars alt-type] (concrete-type alt-type) - #let [[deps alt-type] (type;flatten-function alt-type)] - _ (tc;check alt-type sig-type) - member-type (find-member-type member-idx alt-type) - _ (check-apply member-type input-types output-type) - context' tc;get-context - =deps (M;map @ (provision compiler context') deps)] - (wrap =deps))) - (#;Left error) - (list) - - (#;Right =deps) - (list [alt-name =deps])))) - List/join) - #;Nil - (meta;fail (format "No alternatives for " (%type (type;function input-types output-type)))) - - found - (wrap found)))) - -(def: (find-alternatives sig-type member-idx input-types output-type) - (-> Type Nat (List Type) Type (Meta (List Instance))) - (let [test (test-alternatives sig-type member-idx input-types output-type)] - ($_ meta;either - (do Monad [alts local-env] (test alts)) - (do Monad [alts local-structs] (test alts)) - (do Monad [alts import-structs] (test alts))))) - -(def: (var? input) - (-> Code Bool) - (case input - [_ (#;Symbol _)] - true - - _ - false)) - -(def: (join-pair [l r]) - (All [a] (-> [a a] (List a))) - (list l r)) - -(def: (instance$ [constructor dependencies]) - (-> Instance Code) - (case dependencies - #;Nil - (code;symbol constructor) - - _ - (` ((~ (code;symbol constructor)) (~@ (List/map instance$ dependencies)))))) - -(syntax: #export (::: [member s;symbol] - [args (p;alt (p;seq (p;some s;symbol) s;end!) - (p;seq (p;some s;any) s;end!))]) - {#;doc (doc "Automatic structure selection (for type-class style polymorphism)." - "This feature layers type-class style polymorphism on top of Lux's signatures and structures." - "When calling a polymorphic function, or using a polymorphic constant," - "this macro will check the types of the arguments, and the expected type for the whole expression" - "and it will search in the local scope, the module's scope and the imports' scope" - "in order to find suitable structures to satisfy those requirements." - "If a single alternative is found, that one will be used automatically." - "If no alternative is found, or if more than one alternative is found (ambiguity)" - "a compile-time error will be raised, to alert the user." - "Examples:" - "Nat equality" - (:: number;Eq = x y) - (::: = x y) - "Can optionally add the prefix of the module where the signature was defined." - (::: eq;= x y) - "(List Nat) equality" - (::: = - (list;n.range +1 +10) - (list;n.range +1 +10)) - "(Functor List) map" - (::: map n.inc (list;n.range +0 +9)) - "Caveat emptor: You need to make sure to import the module of any structure you want to use." - "Otherwise, this macro will not find it.")} - (case args - (#;Left [args _]) - (do @ - [[member-idx sig-type] (resolve-member member) - input-types (M;map @ resolve-type args) - output-type meta;expected-type - chosen-ones (find-alternatives sig-type member-idx input-types output-type)] - (case chosen-ones - #;Nil - (meta;fail (format "No structure option could be found for member: " (%ident member))) - - (#;Cons chosen #;Nil) - (wrap (list (` (:: (~ (instance$ chosen)) - (~ (code;local-symbol (product;right member))) - (~@ (List/map code;symbol args)))))) - - _ - (meta;fail (format "Too many options available: " - (|> chosen-ones - (List/map (. %ident product;left)) - (text;join-with ", ")) - " --- for type: " (%type sig-type))))) - - (#;Right [args _]) - (do @ - [labels (M;seq @ (list;repeat (list;size args) - (meta;gensym ""))) - #let [retry (` (let [(~@ (|> (list;zip2 labels args) (List/map join-pair) List/join))] - (;;::: (~ (code;symbol member)) (~@ labels))))]] - (wrap (list retry))) - )) diff --git a/stdlib/source/lux/meta/type/implicit.lux b/stdlib/source/lux/meta/type/implicit.lux new file mode 100644 index 000000000..a2013d3b1 --- /dev/null +++ b/stdlib/source/lux/meta/type/implicit.lux @@ -0,0 +1,363 @@ +(;module: + lux + (lux (control ["M" monad #+ do Monad] + [eq] + ["p" parser]) + (data [text "Text/" Eq] + text/format + [number] + (coll [list "List/" Monad Fold] + [dict]) + [bool] + [product] + [maybe]) + [meta #+ Monad] + (meta [code] + ["s" syntax #+ syntax: Syntax] + [type] + (type ["tc" check #+ Check Monad])) + )) + +(def: (find-type-var id env) + (-> Nat Type-Context (Meta Type)) + (case (list;find (|>. product;left (n.= id)) + (get@ #;var-bindings env)) + (#;Some [_ (#;Some type)]) + (case type + (#;Var id') + (find-type-var id' env) + + _ + (:: Monad wrap type)) + + (#;Some [_ #;None]) + (meta;fail (format "Unbound type-var " (%n id))) + + #;None + (meta;fail (format "Unknown type-var " (%n id))) + )) + +(def: (resolve-type var-name) + (-> Ident (Meta Type)) + (do Monad + [raw-type (meta;find-type var-name) + compiler meta;get-compiler] + (case raw-type + (#;Var id) + (find-type-var id (get@ #;type-context compiler)) + + _ + (wrap raw-type)))) + +(def: (find-member-type idx sig-type) + (-> Nat Type (Check Type)) + (case sig-type + (#;Named _ sig-type') + (find-member-type idx sig-type') + + (#;Apply arg func) + (case (type;apply (list arg) func) + #;None + (tc;fail (format "Cannot apply type " (%type func) " to type " (%type arg))) + + (#;Some sig-type') + (find-member-type idx sig-type')) + + (#;Product left right) + (if (n.= +0 idx) + (:: Monad wrap left) + (find-member-type (n.dec idx) right)) + + _ + (if (n.= +0 idx) + (:: Monad wrap sig-type) + (tc;fail (format "Cannot find member type " (%n idx) " for " (%type sig-type)))))) + +(def: (find-member-name member) + (-> Ident (Meta Ident)) + (case member + ["" simple-name] + (meta;either (do Monad + [member (meta;normalize member) + _ (meta;resolve-tag member)] + (wrap member)) + (do Monad + [this-module-name meta;current-module-name + imp-mods (meta;imported-modules this-module-name) + tag-lists (M;map @ meta;tag-lists imp-mods) + #let [tag-lists (|> tag-lists List/join (List/map product;left) List/join) + candidates (list;filter (. (Text/= simple-name) product;right) + tag-lists)]] + (case candidates + #;Nil + (meta;fail (format "Unknown tag: " (%ident member))) + + (#;Cons winner #;Nil) + (wrap winner) + + _ + (meta;fail (format "Too many candidate tags: " (%list %ident candidates)))))) + + _ + (:: Monad wrap member))) + +(def: (resolve-member member) + (-> Ident (Meta [Nat Type])) + (do Monad + [member (find-member-name member) + [idx tag-list sig-type] (meta;resolve-tag member)] + (wrap [idx sig-type]))) + +(def: (prepare-defs this-module-name defs) + (-> Text (List [Text Def]) (List [Ident Type])) + (|> defs + (list;filter (function [[name [def-type def-anns def-value]]] + (meta;struct? def-anns))) + (List/map (function [[name [def-type def-anns def-value]]] + [[this-module-name name] def-type])))) + +(def: local-env + (Meta (List [Ident Type])) + (do Monad + [local-batches meta;locals + #let [total-locals (List/fold (function [[name type] table] + (dict;put~ name type table)) + (: (dict;Dict Text Type) + (dict;new text;Hash)) + (List/join local-batches))]] + (wrap (|> total-locals + dict;entries + (List/map (function [[name type]] [["" name] type])))))) + +(def: local-structs + (Meta (List [Ident Type])) + (do Monad + [this-module-name meta;current-module-name + defs (meta;defs this-module-name)] + (wrap (prepare-defs this-module-name defs)))) + +(def: import-structs + (Meta (List [Ident Type])) + (do Monad + [this-module-name meta;current-module-name + imp-mods (meta;imported-modules this-module-name) + export-batches (M;map @ (function [imp-mod] + (do @ + [exports (meta;exports imp-mod)] + (wrap (prepare-defs imp-mod exports)))) + imp-mods)] + (wrap (List/join export-batches)))) + +(def: (apply-function-type func arg) + (-> Type Type (Check Type)) + (case func + (#;Named _ func') + (apply-function-type func' arg) + + (#;UnivQ _) + (do Monad + [[id var] tc;var] + (apply-function-type (maybe;assume (type;apply (list var) func)) + arg)) + + (#;Function input output) + (do Monad + [_ (tc;check input arg)] + (wrap output)) + + _ + (tc;fail (format "Invalid function type: " (%type func))))) + +(def: (concrete-type type) + (-> Type (Check [(List Nat) Type])) + (case type + (#;UnivQ _) + (do Monad + [[id var] tc;var + [ids final-output] (concrete-type (maybe;assume (type;apply (list var) type)))] + (wrap [(#;Cons id ids) + final-output])) + + _ + (:: Monad wrap [(list) type]))) + +(def: (check-apply member-type input-types output-type) + (-> Type (List Type) Type (Check [])) + (do Monad + [member-type' (M;fold Monad + (function [input member] + (apply-function-type member input)) + member-type + input-types)] + (tc;check output-type member-type'))) + +(type: #rec Instance + {#constructor Ident + #dependencies (List Instance)}) + +(def: (test-provision provision context dep alts) + (-> (-> Compiler Type-Context Type (Check Instance)) + Type-Context Type (List [Ident Type]) + (Meta (List Instance))) + (do Monad + [compiler meta;get-compiler] + (case (|> alts + (List/map (function [[alt-name alt-type]] + (case (tc;run context + (do Monad + [[tvars alt-type] (concrete-type alt-type) + #let [[deps alt-type] (type;flatten-function alt-type)] + _ (tc;check dep alt-type) + context' tc;get-context + =deps (M;map @ (provision compiler context') deps)] + (wrap =deps))) + (#;Left error) + (list) + + (#;Right =deps) + (list [alt-name =deps])))) + List/join) + #;Nil + (meta;fail (format "No candidates for provisioning: " (%type dep))) + + found + (wrap found)))) + +(def: (provision compiler context dep) + (-> Compiler Type-Context Type (Check Instance)) + (case (meta;run compiler + ($_ meta;either + (do Monad [alts local-env] (test-provision provision context dep alts)) + (do Monad [alts local-structs] (test-provision provision context dep alts)) + (do Monad [alts import-structs] (test-provision provision context dep alts)))) + (#;Left error) + (tc;fail error) + + (#;Right candidates) + (case candidates + #;Nil + (tc;fail (format "No candidates for provisioning: " (%type dep))) + + (#;Cons winner #;Nil) + (:: Monad wrap winner) + + _ + (tc;fail (format "Too many candidates for provisioning: " (%type dep) " --- " (%list (. %ident product;left) candidates)))) + )) + +(def: (test-alternatives sig-type member-idx input-types output-type alts) + (-> Type Nat (List Type) Type (List [Ident Type]) (Meta (List Instance))) + (do Monad + [compiler meta;get-compiler + context meta;type-context] + (case (|> alts + (List/map (function [[alt-name alt-type]] + (case (tc;run context + (do Monad + [[tvars alt-type] (concrete-type alt-type) + #let [[deps alt-type] (type;flatten-function alt-type)] + _ (tc;check alt-type sig-type) + member-type (find-member-type member-idx alt-type) + _ (check-apply member-type input-types output-type) + context' tc;get-context + =deps (M;map @ (provision compiler context') deps)] + (wrap =deps))) + (#;Left error) + (list) + + (#;Right =deps) + (list [alt-name =deps])))) + List/join) + #;Nil + (meta;fail (format "No alternatives for " (%type (type;function input-types output-type)))) + + found + (wrap found)))) + +(def: (find-alternatives sig-type member-idx input-types output-type) + (-> Type Nat (List Type) Type (Meta (List Instance))) + (let [test (test-alternatives sig-type member-idx input-types output-type)] + ($_ meta;either + (do Monad [alts local-env] (test alts)) + (do Monad [alts local-structs] (test alts)) + (do Monad [alts import-structs] (test alts))))) + +(def: (var? input) + (-> Code Bool) + (case input + [_ (#;Symbol _)] + true + + _ + false)) + +(def: (join-pair [l r]) + (All [a] (-> [a a] (List a))) + (list l r)) + +(def: (instance$ [constructor dependencies]) + (-> Instance Code) + (case dependencies + #;Nil + (code;symbol constructor) + + _ + (` ((~ (code;symbol constructor)) (~@ (List/map instance$ dependencies)))))) + +(syntax: #export (::: [member s;symbol] + [args (p;alt (p;seq (p;some s;symbol) s;end!) + (p;seq (p;some s;any) s;end!))]) + {#;doc (doc "Automatic structure selection (for type-class style polymorphism)." + "This feature layers type-class style polymorphism on top of Lux's signatures and structures." + "When calling a polymorphic function, or using a polymorphic constant," + "this macro will check the types of the arguments, and the expected type for the whole expression" + "and it will search in the local scope, the module's scope and the imports' scope" + "in order to find suitable structures to satisfy those requirements." + "If a single alternative is found, that one will be used automatically." + "If no alternative is found, or if more than one alternative is found (ambiguity)" + "a compile-time error will be raised, to alert the user." + "Examples:" + "Nat equality" + (:: number;Eq = x y) + (::: = x y) + "Can optionally add the prefix of the module where the signature was defined." + (::: eq;= x y) + "(List Nat) equality" + (::: = + (list;n.range +1 +10) + (list;n.range +1 +10)) + "(Functor List) map" + (::: map n.inc (list;n.range +0 +9)) + "Caveat emptor: You need to make sure to import the module of any structure you want to use." + "Otherwise, this macro will not find it.")} + (case args + (#;Left [args _]) + (do @ + [[member-idx sig-type] (resolve-member member) + input-types (M;map @ resolve-type args) + output-type meta;expected-type + chosen-ones (find-alternatives sig-type member-idx input-types output-type)] + (case chosen-ones + #;Nil + (meta;fail (format "No structure option could be found for member: " (%ident member))) + + (#;Cons chosen #;Nil) + (wrap (list (` (:: (~ (instance$ chosen)) + (~ (code;local-symbol (product;right member))) + (~@ (List/map code;symbol args)))))) + + _ + (meta;fail (format "Too many options available: " + (|> chosen-ones + (List/map (. %ident product;left)) + (text;join-with ", ")) + " --- for type: " (%type sig-type))))) + + (#;Right [args _]) + (do @ + [labels (M;seq @ (list;repeat (list;size args) + (meta;gensym ""))) + #let [retry (` (let [(~@ (|> (list;zip2 labels args) (List/map join-pair) List/join))] + (;;::: (~ (code;symbol member)) (~@ labels))))]] + (wrap (list retry))) + )) diff --git a/stdlib/test/test/lux/meta/type/auto.lux b/stdlib/test/test/lux/meta/type/auto.lux deleted file mode 100644 index 278bad106..000000000 --- a/stdlib/test/test/lux/meta/type/auto.lux +++ /dev/null @@ -1,41 +0,0 @@ -(;module: - lux - (lux [io] - (control [monad #+ do Monad] - functor - [eq]) - (data [text "Text/" Monoid] - text/format - [number] - [bool "B/" Eq] - maybe - (coll [list])) - ["r" math/random] - (meta [type] - type/auto)) - lux/test) - -(context: "Automatic structure selection" - (<| (times +100) - (do @ - [x r;nat - 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))) - ))) - - (test "Can automatically select second-order structures." - (::: = - (list;n.range +1 +10) - (list;n.range +1 +10))) - - (test "Can automatically select third-order structures." - (let [lln (::: map (list;n.range +1) - (list;n.range +1 +10))] - (::: = lln lln))) - )))) diff --git a/stdlib/test/test/lux/meta/type/implicit.lux b/stdlib/test/test/lux/meta/type/implicit.lux new file mode 100644 index 000000000..8c05b01af --- /dev/null +++ b/stdlib/test/test/lux/meta/type/implicit.lux @@ -0,0 +1,41 @@ +(;module: + lux + (lux [io] + (control [monad #+ do Monad] + functor + [eq]) + (data [text "Text/" Monoid] + text/format + [number] + [bool "B/" Eq] + maybe + (coll [list])) + ["r" math/random] + (meta [type] + type/implicit)) + lux/test) + +(context: "Automatic structure selection" + (<| (times +100) + (do @ + [x r;nat + 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))) + ))) + + (test "Can automatically select second-order structures." + (::: = + (list;n.range +1 +10) + (list;n.range +1 +10))) + + (test "Can automatically select third-order structures." + (let [lln (::: map (list;n.range +1) + (list;n.range +1 +10))] + (::: = lln lln))) + )))) diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux index ea0aa72f7..d4e038774 100644 --- a/stdlib/test/tests.lux +++ b/stdlib/test/tests.lux @@ -68,7 +68,7 @@ ["poly_;" functor]) ["_;" type] (type ["_;" check] - ["_;" auto] + ["_;" implicit] ["_;" object])) (lang ["lang_;" syntax]) (world ["_;" blob] -- cgit v1.2.3