From 35832f8e115e087a949cc5c7b0832cdef43f2d41 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 15 Dec 2016 00:36:58 -0400 Subject: - Updated tests for lux/type. - Added tests for lux/type/check and lux/type/auto. --- stdlib/source/lux.lux | 10 +-- stdlib/source/lux/control/effect.lux | 2 +- stdlib/source/lux/macro/poly.lux | 4 +- stdlib/source/lux/type.lux | 47 ++++++++-- stdlib/source/lux/type/auto.lux | 59 ++++++++++--- stdlib/source/lux/type/check.lux | 16 ++-- stdlib/test/test/lux/type.lux | 164 +++++++++++++++++++++++++++-------- stdlib/test/test/lux/type/auto.lux | 28 ++++++ stdlib/test/test/lux/type/check.lux | 162 ++++++++++++++++++++++++++++++++++ stdlib/test/tests.lux | 16 ++-- 10 files changed, 427 insertions(+), 81 deletions(-) create mode 100644 stdlib/test/test/lux/type/auto.lux create mode 100644 stdlib/test/test/lux/type/check.lux diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux index de985db95..b834649e8 100644 --- a/stdlib/source/lux.lux +++ b/stdlib/source/lux.lux @@ -3254,8 +3254,8 @@ _ (list type)))] - [flatten-sum #;SumT] - [flatten-prod #;ProdT] + [flatten-variant #;SumT] + [flatten-tuple #;ProdT] [flatten-lambda #;LambdaT] [flatten-app #;AppT] ) @@ -3264,7 +3264,7 @@ (-> Type (Maybe (List Type))) (case type (#ProdT _) - (#Some (flatten-prod type)) + (#Some (flatten-tuple type)) (#AppT fun arg) (do Monad @@ -4059,10 +4059,10 @@ "Unit" (#SumT _) - ($_ Text/append "(| " (|> (flatten-sum type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")") + ($_ Text/append "(| " (|> (flatten-variant type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")") (#ProdT _) - ($_ Text/append "[" (|> (flatten-prod type) (map Type/show) (interpose " ") reverse (fold Text/append "")) "]") + ($_ Text/append "[" (|> (flatten-tuple type) (map Type/show) (interpose " ") reverse (fold Text/append "")) "]") (#LambdaT _) ($_ Text/append "(-> " (|> (flatten-lambda type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")") diff --git a/stdlib/source/lux/control/effect.lux b/stdlib/source/lux/control/effect.lux index 16605e1c7..379a28d76 100644 --- a/stdlib/source/lux/control/effect.lux +++ b/stdlib/source/lux/control/effect.lux @@ -300,7 +300,7 @@ (if (tc;checks? (clean-effect effect) eff0) (#;Some idx) #;None)) - (|> unfoldT1 type;flatten-sum (List/map un-apply) list;enumerate)) + (|> unfoldT1 type;flatten-variant (List/map un-apply) list;enumerate)) (#;Some idx)]) (wrap (list (` (#;;Effect (:: (~ g!functor) (~' map) (~' wrap) ((~ (ast;int (nat-to-int idx))) (~ (ast;symbol var)))))))) diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux index 0973eece6..8c3a5b288 100644 --- a/stdlib/source/lux/macro/poly.lux +++ b/stdlib/source/lux/macro/poly.lux @@ -91,8 +91,8 @@ (:: compiler;Monad wrap members) (compiler;fail (format "Not a " ($AST$ ) " type: " (%type :type:)))))))] - [sum sum+ type;flatten-sum #;SumT] - [prod prod+ type;flatten-prod #;ProdT] + [sum sum+ type;flatten-variant #;SumT] + [prod prod+ type;flatten-tuple #;ProdT] ) (def: #export func diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux index c16c8217b..91b44bfd8 100644 --- a/stdlib/source/lux/type.lux +++ b/stdlib/source/lux/type.lux @@ -128,11 +128,11 @@ _ [(list) type])) -(def: #export (flatten-apply type) +(def: #export (flatten-application type) (-> Type [Type (List Type)]) (case type (#;AppT left' right) - (let [[left rights] (flatten-apply left')] + (let [[left rights] (flatten-application left')] [left (List/append rights (list right))]) _ @@ -148,8 +148,8 @@ _ (list type)))] - [flatten-sum #;SumT] - [flatten-prod #;ProdT] + [flatten-variant #;SumT] + [flatten-tuple #;ProdT] ) (def: #export (apply-type type-fun param) @@ -197,8 +197,8 @@ (^template [ ] ( left right) (` ( (~@ (List/map to-ast ( type)))))) - ([#;SumT | flatten-sum] - [#;ProdT & flatten-prod]) + ([#;SumT | flatten-variant] + [#;ProdT & flatten-tuple]) (#;NamedT name sub-type) (ast;symbol name) @@ -236,8 +236,8 @@ (list;interpose " ") (List/fold Text/append "")) )) - ([#;SumT "(| " ")" flatten-sum] - [#;ProdT "[" "]" flatten-prod]) + ([#;SumT "(| " ")" flatten-variant] + [#;ProdT "[" "]" flatten-tuple]) (#;LambdaT input output) (let [[ins out] (flatten-function type)] @@ -259,7 +259,7 @@ ($_ Text/append "⟨e:" (Nat/encode id) "⟩") (#;AppT fun param) - (let [[type-fun type-args] (flatten-apply type)] + (let [[type-fun type-args] (flatten-application type)] ($_ Text/append "(" (to-text type-fun) " " (|> type-args (List/map to-text) list;reverse (list;interpose " ") (List/fold Text/append "")) ")")) (#;UnivQ env body) @@ -306,3 +306,32 @@ [variant Void #;SumT] [tuple Unit #;ProdT] ) + +(def: #export (function inputs output) + (-> (List Type) Type Type) + (case inputs + #;Nil + output + + (#;Cons input inputs') + (#;LambdaT input (function inputs' output)))) + +(def: #export (application quant params) + (-> Type (List Type) Type) + (case params + #;Nil + quant + + (#;Cons param params') + (application (#;AppT quant param) params'))) + +(do-template [ ] + [(def: #export ( size body) + (-> Nat Type Type) + (case size + +0 body + _ ( (list) ( (n.dec size) body))))] + + [univq #;UnivQ] + [exq #;ExQ] + ) diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux index f33314ac1..c22434e9f 100644 --- a/stdlib/source/lux/type/auto.lux +++ b/stdlib/source/lux/type/auto.lux @@ -20,6 +20,37 @@ (type ["tc" check #+ Check Monad]) )) +(def: (find-type-var id env) + (-> Nat (Bindings Nat (Maybe Type)) (Lux Type)) + (case (list;find (|>. product;left (n.= id)) + (get@ #;mappings env)) + (#;Some [_ (#;Some type)]) + (case type + (#;VarT id') + (find-type-var id' env) + + _ + (:: Monad wrap type)) + + (#;Some [_ #;None]) + (compiler;fail (format "Unbound type-var " (%n id))) + + #;None + (compiler;fail (format "Unknown type-var " (%n id))) + )) + +(def: (resolve-type var-name) + (-> Ident (Lux Type)) + (do Monad + [raw-type (compiler;find-type var-name) + compiler compiler;get-compiler] + (case raw-type + (#;VarT id) + (find-type-var id (get@ #;type-vars compiler)) + + _ + (wrap raw-type)))) + (def: (find-member-type idx sig-type) (-> Nat Type (Check Type)) (case sig-type @@ -84,8 +115,12 @@ (do Monad [this-module-name compiler;current-module-name imp-mods (compiler;imported-modules this-module-name) - export-batches (mapM @ compiler;exports imp-mods)] - (wrap (prepare-defs this-module-name (List/join export-batches))))) + export-batches (mapM @ (lambda [imp-mod] + (do @ + [exports (compiler;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)) @@ -123,7 +158,7 @@ (lambda [compiler] (let [type-vars (get@ #;type-vars compiler) context (|> tc;fresh-context - (set@ #tc;var-id (get@ #;counter type-vars)) + (set@ #tc;var-counter (get@ #;counter type-vars)) (set@ #tc;bindings (dict;from-list number;Hash (get@ #;mappings type-vars))))] (#;Right [compiler context])))) @@ -135,7 +170,7 @@ (list;filter (lambda [[alt-name alt-type]] (case (tc;run context (do Monad - [_ (tc;check sig-type 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))) (#;Left error) @@ -171,23 +206,23 @@ (All [a] (-> [a a] (List a))) (list l r)) -(syntax: #export (::: {member s;symbol} - {args (s;alt (s;some s;symbol) - (s;some s;any))}) +(syntax: #export (::: [member s;symbol] + [args (s;alt (s;some s;symbol) + (s;some s;any))]) (case args (#;Left args) (do @ [[member-idx sig-type] (resolve-member member) - input-types (mapM @ compiler;find-type args) + input-types (mapM @ resolve-type args) output-type compiler;expected-type chosen-ones (find-alternatives sig-type member-idx input-types output-type)] (case chosen-ones #;Nil - (compiler;fail (format "No structure option could be found for member " (%ident member))) + (compiler;fail (format "No structure option could be found for member: " (%ident member))) (#;Cons chosen #;Nil) (wrap (list (` (:: (~ (ast;symbol chosen)) - (~ (ast;symbol member)) + (~ (ast;local-symbol (product;right member))) (~@ (List/map ast;symbol args)))))) _ @@ -205,7 +240,3 @@ #let [retry (` (let [(~@ (|> (list;zip2 labels args-to-bind) (List/map join-pair) List/join))] (;;::: (~ (ast;symbol member)) (~@ labels))))]] (wrap (list retry))))) - -(comment - (::: map i.inc (list 0 1 2 3 4)) - ) diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux index 951586bb0..b9a1301bc 100644 --- a/stdlib/source/lux/type/check.lux +++ b/stdlib/source/lux/type/check.lux @@ -24,8 +24,8 @@ (type: #export Fixpoints (List [[Type Type] Bool])) (type: #export Context - {#var-id Id - #ex-id Id + {#var-counter Id + #ex-counter Id #bindings (dict;Dict Id (Maybe Type)) #fixpoints Fixpoints }) @@ -111,8 +111,8 @@ (def: #export existential (Check [Id Type]) (lambda [context] - (let [id (get@ #ex-id context)] - (#;Right [(update@ #ex-id n.inc context) + (let [id (get@ #ex-counter context)] + (#;Right [(update@ #ex-counter n.inc context) [id (#;ExT id)]])))) (def: (bound? id) @@ -241,9 +241,9 @@ (def: #export create-var (Check [Id Type]) (lambda [context] - (let [id (get@ #var-id context)] + (let [id (get@ #var-counter context)] (#;Right [(|> context - (update@ #var-id n.inc) + (update@ #var-counter n.inc) (update@ #bindings (dict;put id #;None))) [id (#;VarT id)]])))) @@ -307,8 +307,8 @@ (def: #export fresh-context Context - {#var-id +0 - #ex-id +0 + {#var-counter +0 + #ex-counter +0 #bindings (dict;new number;Hash) #fixpoints (list) }) diff --git a/stdlib/test/test/lux/type.lux b/stdlib/test/test/lux/type.lux index 8fa871e70..0e203f376 100644 --- a/stdlib/test/test/lux/type.lux +++ b/stdlib/test/test/lux/type.lux @@ -1,41 +1,137 @@ +## Copyright (c) Eduardo Julian. All rights reserved. +## This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +## If a copy of the MPL was not distributed with this file, +## You can obtain one at http://mozilla.org/MPL/2.0/. + (;module: lux (lux (codata [io]) (control monad) (data [text "Text/" Monoid] - [number]) - type - (codata function)) + text/format + [number] + maybe + (struct [list])) + (math ["R" random]) + pipe + ["&" type]) lux/test) -(test: "lux/type exports" - (let% [ (do-template [] - [(match true (:: Eq = ))] - - [(#;HostT "java.util.List" (list Int))] - [#;UnitT] - [#;VoidT] - [(#;VarT +123)] - [(#;ExT +123)] - [(#;BoundT +123)] - [(#;LambdaT Bool Int)] - [(#;AppT List Int)] - [(#;NamedT ["" "Int-List"] (#;AppT List Int))] - [(#;SumT Bool Int)] - [(#;ProdT Bool Int)] - [(#;UnivQ (list) (#;ProdT Bool (#;BoundT +1)))] - [(#;ExQ (list) (#;ProdT Bool (#;BoundT +1)))] - )] - (test-all - (match (^=> (#;Some _type) (:: Eq = _type (#;ProdT Bool Int))) - (apply-type (type (Meta Bool)) Int)) - (match #;None (apply-type Text Bool)) - (match true - (:: Eq = - (#;NamedT ["" "a"] - (#;ProdT Bool Int)) - (un-alias (#;NamedT ["" "c"] - (#;NamedT ["" "b"] - (#;NamedT ["" "a"] - (#;ProdT Bool Int))))))) - ))) +## [Utils] +(def: gen-name + (R;Random Text) + (do R;Monad + [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 (lambda [gen-type] + ($_ R;alt + (R;seq gen-name (R/wrap (list))) + (R/wrap []) + (R/wrap []) + (R;seq gen-type gen-type) + (R;seq gen-type gen-type) + (R;seq gen-type gen-type) + R;nat + R;nat + R;nat + (R;seq (R/wrap (list)) gen-type) + (R;seq (R/wrap (list)) gen-type) + (R;seq gen-type gen-type) + (R;seq gen-ident gen-type) + ))))) + +## [Tests] +(test: "Types" + [sample gen-type] + (assert "Every type is equal to itself." + (:: &;Eq = sample sample))) + +(test: "Type application" + (assert "Can apply quantified types (universal and existential quantification)." + (and (default false + (do Monad + [partial (&;apply-type Meta Bool) + full (&;apply-type partial Int)] + (wrap (:: &;Eq = full (#;ProdT Bool Int))))) + (|> (&;apply-type Text Bool) + (case> #;None true _ false))))) + +(test: "Naming" + (let [base (#;NamedT ["" "a"] (#;ProdT Bool Int)) + aliased (#;NamedT ["" "c"] + (#;NamedT ["" "b"] + base))] + ($_ seq + (assert "Can remove aliases from an already-named type." + (:: &;Eq = + base + (&;un-alias aliased))) + + (assert "Can remove all names from a type." + (and (not (:: &;Eq = + base + (&;un-name aliased))) + (:: &;Eq = + (&;un-name base) + (&;un-name aliased))))))) + +(test: "Type construction [structs]" + [size (|> R;nat (:: @ map (n.% +3))) + members (seqM @ (list;repeat size gen-type)) + #let [(^open "&/") &;Eq + (^open "L/") (list;Eq &;Eq)]] + (let% [ (do-template [ ] + [(assert (format "Can build and tear-down " " types.") + (let [flat (|> members )] + (or (n.= (list;size members) (list;size flat)) + (and (n.= +0 (list;size members)) + (n.= +1 (list;size flat)) + (|> flat list;head (default (undefined)) (&/= ))))))] + + ["variant" &;variant &;flatten-variant #;VoidT] + ["tuple" &;tuple &;flatten-tuple #;UnitT] + )] + ($_ seq + + ))) + +(test: "Type construction [parameterized]" + [size (|> R;nat (:: @ map (n.% +3))) + members (seqM @ (list;repeat size gen-type)) + extra gen-type + #let [(^open "&/") &;Eq + (^open "L/") (list;Eq &;Eq)]] + ($_ seq + (assert "Can build and tear-down function types." + (let [[inputs output] (|> (&;function members extra) &;flatten-function)] + (n.= (list;size members) (list;size inputs)))) + + (assert "Can build and tear-down application types." + (let [[tfunc tparams] (|> members (&;application extra) &;flatten-application)] + (n.= (list;size members) (list;size tparams)))) + )) + +(test: "Type construction [higher order]" + [size (|> R;nat (:: @ map (n.% +3))) + extra gen-type + #let [(^open "&/") &;Eq]] + (let% [ (do-template [ ] + [(assert (format "Can build and tear-down " " types.") + (let [[flat-size flat-body] (|> extra ( size) )] + (and (n.= size flat-size) + (&/= extra flat-body))))] + + ["universally-quantified" &;univq &;flatten-univq] + ["existentially-quantified" &;exq &;flatten-exq] + )] + ($_ seq + + ))) diff --git a/stdlib/test/test/lux/type/auto.lux b/stdlib/test/test/lux/type/auto.lux new file mode 100644 index 000000000..ef69961cd --- /dev/null +++ b/stdlib/test/test/lux/type/auto.lux @@ -0,0 +1,28 @@ +## Copyright (c) Eduardo Julian. All rights reserved. +## This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +## If a copy of the MPL was not distributed with this file, +## You can obtain one at http://mozilla.org/MPL/2.0/. + +(;module: + lux + (lux (codata [io]) + (control monad + [eq]) + (data [text "Text/" Monoid] + text/format + [number] + [bool "B/" Eq] + maybe + (struct [list])) + (math ["R" random]) + pipe + [type] + type/auto) + lux/test) + +(test: "Automatic structure selection" + [x R;nat + y R;nat] + (assert "Can automatically select first-order structures." + (B/= (:: number;Eq = x y) + (::: eq;= x y)))) diff --git a/stdlib/test/test/lux/type/check.lux b/stdlib/test/test/lux/type/check.lux new file mode 100644 index 000000000..273dbad4c --- /dev/null +++ b/stdlib/test/test/lux/type/check.lux @@ -0,0 +1,162 @@ +## Copyright (c) Eduardo Julian. All rights reserved. +## This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +## If a copy of the MPL was not distributed with this file, +## You can obtain one at http://mozilla.org/MPL/2.0/. + +(;module: + lux + (lux (codata [io]) + (control monad) + (data [text "Text/" Monoid] + text/format + [number] + maybe + (struct [list])) + (math ["R" random]) + pipe + [type] + ["&" 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 (lambda [gen-type] + ($_ R;alt + (R;seq gen-name (R/wrap (list))) + (R/wrap []) + (R/wrap []) + (R;seq gen-type gen-type) + (R;seq gen-type gen-type) + (R;seq gen-type gen-type) + R;nat + R;nat + R;nat + (R;seq (R/wrap (list)) gen-type) + (R;seq (R/wrap (list)) gen-type) + (R;seq gen-type gen-type) + (R;seq gen-ident gen-type) + ))))) + +(def: (type-checks? input) + (-> (&;Check []) Bool) + (case (&;run &;fresh-context input) + (#;Right []) + true + + (#;Left error) + false)) + +## [Tests] +(test: "Top and Bottom" + [sample gen-type] + ($_ seq + (assert "Top is the super-type 0f everything." + (&;checks? Top sample)) + + (assert "Bottom is the sub-type 0f everything." + (&;checks? sample Bottom)) + )) + +(test: "Simple type-checking." + ($_ seq + (assert "Unit and Void match themselves." + (and (&;checks? Void Void) + (&;checks? Unit Unit))) + + (assert "Existential types only match with themselves." + (and (type-checks? (do &;Monad + [[id ex] &;existential] + (&;check ex ex))) + (not (type-checks? (do &;Monad + [[lid lex] &;existential + [rid rex] &;existential] + (&;check lex rex)))))) + + (assert "Names don't affect type-checking." + (and (type-checks? (do &;Monad + [[id ex] &;existential] + (&;check (#;NamedT ["module" "name"] ex) + ex))) + (type-checks? (do &;Monad + [[id ex] &;existential] + (&;check ex + (#;NamedT ["module" "name"] ex)))) + (type-checks? (do &;Monad + [[id ex] &;existential] + (&;check (#;NamedT ["module" "name"] ex) + (#;NamedT ["module" "name"] ex)))))) + + (assert "Can type-check functions." + (and (&;checks? (#;LambdaT Bottom Top) + (#;LambdaT Top Bottom)) + (not (&;checks? (#;LambdaT Top Bottom) + (#;LambdaT Bottom Top))))) + )) + +(test: "Type application" + [meta gen-type + data gen-type] + (assert "Can type-check type application." + (and (&;checks? (#;AppT (#;AppT Meta meta) data) + (type;tuple (list meta data))) + (&;checks? (type;tuple (list meta data)) + (#;AppT (#;AppT Meta meta) data))))) + +(test: "Host types" + [nameL gen-name + nameR gen-name + paramL gen-type + paramR gen-type] + ($_ seq + (assert "Host types match when they have the same name and the same parameters." + (&;checks? (#;HostT nameL (list paramL)) + (#;HostT nameL (list paramL)))) + + (assert "Names matter to host types." + (&;checks? (#;HostT nameL (list paramL)) + (#;HostT nameR (list paramL)))) + + (assert "Parameters matter to host types." + (&;checks? (#;HostT nameL (list paramL)) + (#;HostT nameL (list paramR)))) + )) + +(test: "Type-vars" + ($_ seq + (assert "Type-vars check against themselves." + (type-checks? (&;with-var (lambda [[id var]] (&;check var var))))) + + (assert "Can bind unbound type-vars by type-checking against them." + (and (type-checks? (&;with-var (lambda [[id var]] (&;check var #;UnitT)))) + (type-checks? (&;with-var (lambda [[id var]] (&;check #;UnitT var)))))) + + (assert "Can't rebind already bound type-vars." + (not (type-checks? (&;with-var (lambda [[id var]] + (do &;Monad + [_ (&;check var #;UnitT)] + (&;check var #;VoidT))))))) + + (assert "If the type bound to a var is a super-type to another, then the var is also a super-type." + (type-checks? (&;with-var (lambda [[id var]] + (do &;Monad + [_ (&;check var Top)] + (&;check var #;UnitT)))))) + + (assert "If the type bound to a var is a sub-type of another, then the var is also a sub-type." + (type-checks? (&;with-var (lambda [[id var]] + (do &;Monad + [_ (&;check var Bottom)] + (&;check #;UnitT var)))))) + )) diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux index e225e1f28..ef94dca90 100644 --- a/stdlib/test/tests.lux +++ b/stdlib/test/tests.lux @@ -59,17 +59,17 @@ (macro ["_;" ast] ["_;" syntax] ["_;" template]) - ## [type] - ## (type [check] [auto]) - ## (control ...) + ["_;" type] + (type ["_;" check] + ["_;" auto]) + ## (control [effect]) ) ) ## (lux (codata [cont]) - ## (macro [poly] - ## (poly ["poly_;" eq] - ## ["poly_;" text-encoder] - ## ["poly_;" functor])) - ## (control [effect])) + ## (macro [poly] + ## (poly ["poly_;" eq] + ## ["poly_;" text-encoder] + ## ["poly_;" functor]))) ) ## [Program] -- cgit v1.2.3