diff options
Diffstat (limited to 'new-luxc/test/test/luxc/analyser/function.lux')
| -rw-r--r-- | new-luxc/test/test/luxc/analyser/function.lux | 178 |
1 files changed, 91 insertions, 87 deletions
diff --git a/new-luxc/test/test/luxc/analyser/function.lux b/new-luxc/test/test/luxc/analyser/function.lux index 4b74db183..baef5c42c 100644 --- a/new-luxc/test/test/luxc/analyser/function.lux +++ b/new-luxc/test/test/luxc/analyser/function.lux @@ -64,92 +64,96 @@ false))) (context: "Function definition." - [func-name (r;text +5) - arg-name (|> (r;text +5) (r;filter (|>. (text/= func-name) not))) - [outputT outputC] gen-primitive - [inputT _] gen-primitive] - ($_ seq - (test "Can analyse function." - (|> (&;with-expected-type (type (All [a] (-> a outputT))) - (@;analyse-function analyse func-name arg-name outputC)) - (meta;run (init-compiler [])) - succeeds?)) - (test "Generic functions can always be specialized." - (and (|> (&;with-expected-type (-> inputT outputT) - (@;analyse-function analyse func-name arg-name outputC)) - (meta;run (init-compiler [])) - succeeds?) - (|> (&;with-expected-type (-> inputT inputT) - (@;analyse-function analyse func-name arg-name (code;symbol ["" arg-name]))) - (meta;run (init-compiler [])) - succeeds?))) - (test "Can infer function (constant output and unused input)." - (|> (@common;with-unknown-type - (@;analyse-function analyse func-name arg-name outputC)) - (meta;run (init-compiler [])) - (check-type (type (All [a] (-> a outputT)))))) - (test "Can infer function (output = input)." - (|> (@common;with-unknown-type - (@;analyse-function analyse func-name arg-name (code;symbol ["" arg-name]))) - (meta;run (init-compiler [])) - (check-type (type (All [a] (-> a a)))))) - (test "The function's name is bound to the function's type." - (|> (&;with-expected-type (type (Rec self (-> inputT self))) - (@;analyse-function analyse func-name arg-name (code;symbol ["" func-name]))) - (meta;run (init-compiler [])) - succeeds?)) - (test "Can infer recursive types for functions." - (|> (@common;with-unknown-type - (@;analyse-function analyse func-name arg-name (code;symbol ["" func-name]))) - (meta;run (init-compiler [])) - (check-type (type (Rec self (All [a] (-> a self))))))) - )) + (<| (times +100) + (do @ + [func-name (r;text +5) + arg-name (|> (r;text +5) (r;filter (|>. (text/= func-name) not))) + [outputT outputC] gen-primitive + [inputT _] gen-primitive] + ($_ seq + (test "Can analyse function." + (|> (&;with-expected-type (type (All [a] (-> a outputT))) + (@;analyse-function analyse func-name arg-name outputC)) + (meta;run (init-compiler [])) + succeeds?)) + (test "Generic functions can always be specialized." + (and (|> (&;with-expected-type (-> inputT outputT) + (@;analyse-function analyse func-name arg-name outputC)) + (meta;run (init-compiler [])) + succeeds?) + (|> (&;with-expected-type (-> inputT inputT) + (@;analyse-function analyse func-name arg-name (code;symbol ["" arg-name]))) + (meta;run (init-compiler [])) + succeeds?))) + (test "Can infer function (constant output and unused input)." + (|> (@common;with-unknown-type + (@;analyse-function analyse func-name arg-name outputC)) + (meta;run (init-compiler [])) + (check-type (type (All [a] (-> a outputT)))))) + (test "Can infer function (output = input)." + (|> (@common;with-unknown-type + (@;analyse-function analyse func-name arg-name (code;symbol ["" arg-name]))) + (meta;run (init-compiler [])) + (check-type (type (All [a] (-> a a)))))) + (test "The function's name is bound to the function's type." + (|> (&;with-expected-type (type (Rec self (-> inputT self))) + (@;analyse-function analyse func-name arg-name (code;symbol ["" func-name]))) + (meta;run (init-compiler [])) + succeeds?)) + (test "Can infer recursive types for functions." + (|> (@common;with-unknown-type + (@;analyse-function analyse func-name arg-name (code;symbol ["" func-name]))) + (meta;run (init-compiler [])) + (check-type (type (Rec self (All [a] (-> a self))))))) + )))) (context: "Function application." - [full-args (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2)))) - partial-args (|> r;nat (:: @ map (n.% full-args))) - var-idx (|> r;nat (:: @ map (|>. (n.% full-args) (n.max +1)))) - inputsTC (r;list full-args gen-primitive) - #let [inputsT (list/map product;left inputsTC) - inputsC (list/map product;right inputsTC)] - [outputT outputC] gen-primitive - #let [funcT (type;function inputsT outputT) - partialT (type;function (list;drop partial-args inputsT) outputT) - varT (#;Bound +1) - polyT (<| (type;univ-q +1) - (type;function (list;concat (list (list;take var-idx inputsT) - (list varT) - (list;drop (n.inc var-idx) inputsT)))) - varT) - poly-inputT (maybe;assume (list;nth var-idx inputsT)) - partial-poly-inputsT (list;drop (n.inc var-idx) inputsT) - partial-polyT1 (<| (type;function partial-poly-inputsT) - poly-inputT) - partial-polyT2 (<| (type;univ-q +1) - (type;function (#;Cons varT partial-poly-inputsT)) - varT)]] - ($_ seq - (test "Can analyse monomorphic type application." - (|> (@common;with-unknown-type - (@;analyse-apply analyse funcT (#la;Unit) inputsC)) - (check-apply outputT full-args))) - (test "Can partially apply functions." - (|> (@common;with-unknown-type - (@;analyse-apply analyse funcT (#la;Unit) - (list;take partial-args inputsC))) - (check-apply partialT partial-args))) - (test "Can apply polymorphic functions." - (|> (@common;with-unknown-type - (@;analyse-apply analyse polyT (#la;Unit) inputsC)) - (check-apply poly-inputT full-args))) - (test "Polymorphic partial application propagates found type-vars." - (|> (@common;with-unknown-type - (@;analyse-apply analyse polyT (#la;Unit) - (list;take (n.inc var-idx) inputsC))) - (check-apply partial-polyT1 (n.inc var-idx)))) - (test "Polymorphic partial application preserves quantification for type-vars." - (|> (@common;with-unknown-type - (@;analyse-apply analyse polyT (#la;Unit) - (list;take var-idx inputsC))) - (check-apply partial-polyT2 var-idx))) - )) + (<| (times +100) + (do @ + [full-args (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2)))) + partial-args (|> r;nat (:: @ map (n.% full-args))) + var-idx (|> r;nat (:: @ map (|>. (n.% full-args) (n.max +1)))) + inputsTC (r;list full-args gen-primitive) + #let [inputsT (list/map product;left inputsTC) + inputsC (list/map product;right inputsTC)] + [outputT outputC] gen-primitive + #let [funcT (type;function inputsT outputT) + partialT (type;function (list;drop partial-args inputsT) outputT) + varT (#;Bound +1) + polyT (<| (type;univ-q +1) + (type;function (list;concat (list (list;take var-idx inputsT) + (list varT) + (list;drop (n.inc var-idx) inputsT)))) + varT) + poly-inputT (maybe;assume (list;nth var-idx inputsT)) + partial-poly-inputsT (list;drop (n.inc var-idx) inputsT) + partial-polyT1 (<| (type;function partial-poly-inputsT) + poly-inputT) + partial-polyT2 (<| (type;univ-q +1) + (type;function (#;Cons varT partial-poly-inputsT)) + varT)]] + ($_ seq + (test "Can analyse monomorphic type application." + (|> (@common;with-unknown-type + (@;analyse-apply analyse funcT (#la;Unit) inputsC)) + (check-apply outputT full-args))) + (test "Can partially apply functions." + (|> (@common;with-unknown-type + (@;analyse-apply analyse funcT (#la;Unit) + (list;take partial-args inputsC))) + (check-apply partialT partial-args))) + (test "Can apply polymorphic functions." + (|> (@common;with-unknown-type + (@;analyse-apply analyse polyT (#la;Unit) inputsC)) + (check-apply poly-inputT full-args))) + (test "Polymorphic partial application propagates found type-vars." + (|> (@common;with-unknown-type + (@;analyse-apply analyse polyT (#la;Unit) + (list;take (n.inc var-idx) inputsC))) + (check-apply partial-polyT1 (n.inc var-idx)))) + (test "Polymorphic partial application preserves quantification for type-vars." + (|> (@common;with-unknown-type + (@;analyse-apply analyse polyT (#la;Unit) + (list;take var-idx inputsC))) + (check-apply partial-polyT2 var-idx))) + )))) |