aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/test')
-rw-r--r--stdlib/source/test/lux/target/python.lux27
-rw-r--r--stdlib/source/test/lux/tool.lux4
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux2
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux1
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux360
5 files changed, 271 insertions, 123 deletions
diff --git a/stdlib/source/test/lux/target/python.lux b/stdlib/source/test/lux/target/python.lux
index 39c51b2a7..6eed5ecab 100644
--- a/stdlib/source/test/lux/target/python.lux
+++ b/stdlib/source/test/lux/target/python.lux
@@ -324,6 +324,31 @@
(list (/.float float/0) (/.float float/1) (/.float float/2)))))
)))
+(def: test|var
+ Test
+ (do [! random.monad]
+ [expected/0 random.safe_frac
+ expected/1 random.safe_frac
+ choice (# ! each (n.% 2) random.nat)
+ .let [expected/? (case choice
+ 0 expected/0
+ _ expected/1)]
+ $var (# ! each (|>> %.nat (format "v") /.var) random.nat)
+ $choice (# ! each (|>> %.nat (format "c") /.var) random.nat)]
+ ($_ _.and
+ (_.cover [/.Single /.SVar /.var]
+ (expression (|>> (:as Frac) (f.= expected/0))
+ (/.apply/* (/.lambda (list $var) $var)
+ (list (/.float expected/0)))))
+ (_.cover [/.Poly /.PVar /.poly]
+ (expression (|>> (:as Frac) (f.= expected/?))
+ (/.apply/* (/.lambda (list $choice (/.poly $var))
+ (/.item $choice $var))
+ (list (/.int (.int choice))
+ (/.float expected/0)
+ (/.float expected/1)))))
+ )))
+
(def: test|expression
Test
(do [! random.monad]
@@ -335,6 +360,8 @@
(_.for [/.Computation]
..test|computation)
..test|function
+ (_.for [/.Var]
+ ..test|var)
))))
(def: .public test
diff --git a/stdlib/source/test/lux/tool.lux b/stdlib/source/test/lux/tool.lux
index 0f42f81db..c9a5cfb7c 100644
--- a/stdlib/source/test/lux/tool.lux
+++ b/stdlib/source/test/lux/tool.lux
@@ -17,7 +17,8 @@
["[1]/[0]" analysis "_"
["[1]/[0]" simple]
["[1]/[0]" complex]
- ["[1]/[0]" reference]]
+ ["[1]/[0]" reference]
+ ["[1]/[0]" function]]
... ["[1]/[0]" synthesis]
]]]
["[1][0]" meta "_"
@@ -41,6 +42,7 @@
/phase/analysis/simple.test
/phase/analysis/complex.test
/phase/analysis/reference.test
+ /phase/analysis/function.test
... /syntax.test
... /synthesis.test
))
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 fa3df9c67..97bdb7a54 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
@@ -78,7 +78,7 @@
{try.#Failure error}
(text.contains? (value@ exception.#label exception) error)))
-(def: simple_parameter
+(def: .public simple_parameter
(Random [Type Code])
(`` ($_ random.either
(~~ (template [<type> <random> <code>]
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 f559e98c4..ed111c5e4 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
@@ -230,7 +230,6 @@
(list.item tag)
(maybe.else ""))]]
($_ _.and
- ..test|sum
(_.cover [/.variant]
(let [expected_variant? (: (-> Symbol Bit)
(function (_ tag)
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 815b488fe..50fbc1c50 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
@@ -1,133 +1,253 @@
(.using
+ [library
[lux "*"
- [abstract
- ["[0]" monad {"+" do}]]
- [data
- ["%" text/format {"+" format}]]
- ["r" math/random {"+" Random}]
["_" test {"+" Test}]
+ [abstract
+ [monad {"+" do}]]
[control
- pipe
- ["[0]" maybe]
- ["[0]" try]]
+ [pipe {"+" case>}]
+ ["[0]" function]
+ ["[0]" try ("[1]#[0]" functor)]
+ ["[0]" exception]]
[data
["[0]" product]
- ["[0]" text ("[1]#[0]" equivalence)]
- [number
- ["n" nat]]
+ ["[0]" text
+ ["%" format]]
[collection
- ["[0]" list ("[1]#[0]" functor)]]]
- ["[0]" type]
- ["[0]" macro
+ ["[0]" list]]]
+ [macro
["[0]" code]]
+ [math
+ ["[0]" random]
+ [number
+ ["n" nat]]]
[meta
- ["[0]" symbol]]]
- [//
- ["_[0]" primitive]
- ["_[0]" structure]]
- [\\
- ["[0]" /
- ["/[1]" //
- ["[1][0]" module]
- ["[1][0]" type]
- ["/[1]" // "_"
- ["/[1]" //
- ["[1][0]" analysis {"+" Analysis Operation}]
- [///
- ["[1][0]" reference]
- ["[0]" phase]
- [meta
- ["[0]" archive]]]]]]]])
-
-(def: (check_apply expectedT num_args analysis)
- (-> Type Nat (Operation Analysis) Bit)
- (|> analysis
- (//type.with_type expectedT)
- (phase.result _primitive.state)
- (case> {try.#Success applyA}
- (let [[funcA argsA] (////analysis.application applyA)]
- (n.= num_args (list.size argsA)))
-
- {try.#Failure _}
- false)))
-
-(def: abstraction
- (do r.monad
- [func_name (r.unicode 5)
- arg_name (|> (r.unicode 5) (r.only (|>> (text#= func_name) not)))
- [outputT outputC] _primitive.primitive
- [inputT _] _primitive.primitive
- .let [g!arg (code.local_symbol arg_name)]]
- (<| (_.context (%.symbol (symbol /.function)))
- ($_ _.and
- (_.test "Can analyse function."
- (and (|> (//type.with_type (All (_ a) (-> a outputT))
- (/.function _primitive.phase func_name arg_name archive.empty outputC))
- _structure.check_succeeds)
- (|> (//type.with_type (All (_ a) (-> a a))
- (/.function _primitive.phase func_name arg_name archive.empty g!arg))
- _structure.check_succeeds)))
- (_.test "Generic functions can always be specialized."
- (and (|> (//type.with_type (-> inputT outputT)
- (/.function _primitive.phase func_name arg_name archive.empty outputC))
- _structure.check_succeeds)
- (|> (//type.with_type (-> inputT inputT)
- (/.function _primitive.phase func_name arg_name archive.empty g!arg))
- _structure.check_succeeds)))
- (_.test "The function's name is bound to the function's type."
- (|> (//type.with_type (Rec self (-> inputT self))
- (/.function _primitive.phase func_name arg_name archive.empty (code.local_symbol func_name)))
- _structure.check_succeeds))
- ))))
+ ["[0]" symbol "_"
+ ["$[1]" \\test]]]
+ ["[0]" type ("[1]#[0]" equivalence)
+ ["$[1]" \\test]
+ ["[0]" check]]]]
+ [\\library
+ ["[0]" /
+ ["/[1]" //
+ [//
+ ["[1][0]" extension
+ ["[1]/[0]" analysis "_"
+ ["[1]" lux]]]
+ [//
+ ["[1][0]" analysis {"+" Analysis}
+ [evaluation {"+" Eval}]
+ ["[2][0]" macro]
+ ["[2][0]" scope]
+ ["[2][0]" module]
+ ["[2][0]" type
+ ["$[1]" \\test]]
+ ["[2][0]" inference "_"
+ ["$[1]" \\test]]]
+ [///
+ ["[1][0]" phase ("[1]#[0]" monad)]
+ [meta
+ ["[0]" archive]]]]]]]])
-(def: apply
- (do [! r.monad]
- [full_args (|> r.nat (# ! each (|>> (n.% 10) (n.max 2))))
- partial_args (|> r.nat (# ! each (n.% full_args)))
- var_idx (|> r.nat (# ! each (|>> (n.% full_args) (n.max 1))))
- inputsTC (r.list full_args _primitive.primitive)
- .let [inputsT (list#each product.left inputsTC)
- inputsC (list#each product.right inputsTC)]
- [outputT outputC] _primitive.primitive
- .let [funcT (type.function inputsT outputT)
- partialT (type.function (list.after partial_args inputsT) outputT)
- varT {.#Parameter 1}
- polyT (<| (type.univ_q 1)
- (type.function (list.together (list (list.first var_idx inputsT)
- (list varT)
- (list.after (++ var_idx) inputsT))))
- varT)
- poly_inputT (maybe.trusted (list.item var_idx inputsT))
- partial_poly_inputsT (list.after (++ var_idx) inputsT)
- partial_polyT1 (<| (type.function partial_poly_inputsT)
- poly_inputT)
- partial_polyT2 (<| (type.univ_q 1)
- (type.function {.#Item varT partial_poly_inputsT})
- varT)
- dummy_function {////analysis.#Function (list) {////analysis.#Reference (////reference.local 1)}}]]
- (<| (_.context (%.symbol (symbol /.apply)))
- ($_ _.and
- (_.test "Can analyse monomorphic type application."
- (|> (/.apply _primitive.phase inputsC funcT dummy_function archive.empty (' []))
- (check_apply outputT full_args)))
- (_.test "Can partially apply functions."
- (|> (/.apply _primitive.phase (list.first partial_args inputsC) funcT dummy_function archive.empty (' []))
- (check_apply partialT partial_args)))
- (_.test "Can apply polymorphic functions."
- (|> (/.apply _primitive.phase inputsC polyT dummy_function archive.empty (' []))
- (check_apply poly_inputT full_args)))
- (_.test "Polymorphic partial application propagates found type-vars."
- (|> (/.apply _primitive.phase (list.first (++ var_idx) inputsC) polyT dummy_function archive.empty (' []))
- (check_apply partial_polyT1 (++ var_idx))))
- (_.test "Polymorphic partial application preserves quantification for type-vars."
- (|> (/.apply _primitive.phase (list.first var_idx inputsC) polyT dummy_function archive.empty (' []))
- (check_apply partial_polyT2 var_idx)))
- ))))
+(def: (eval archive type term)
+ Eval
+ (//phase#in []))
+
+(def: (expander macro inputs state)
+ //macro.Expander
+ {try.#Success ((.macro macro) inputs state)})
+
+(def: analysis
+ //analysis.Phase
+ (//.phase ..expander))
+
+(def: test|function
+ Test
+ (do [! random.monad]
+ [lux $//type.random_state
+ .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]]
+ input/0 ($type.random 0)
+ input/1 ($type.random 0)
+ function/0 (random.ascii/lower 1)
+ function/1 (random.ascii/lower 2)
+ argument/0 (random.ascii/lower 3)
+ argument/1 (random.ascii/lower 4)
+ module/0 (random.ascii/lower 5)
+ [output/0 term/0] $//inference.simple_parameter
+ [output/1 term/1] (random.only (|>> product.left (same? output/0) not)
+ $//inference.simple_parameter)
+ name/0 ($symbol.random 1 1)
+ .let [$function/0 (code.local_symbol function/0)
+ $function/1 (code.local_symbol function/1)
+ $argument/0 (code.local_symbol argument/0)
+ $argument/1 (code.local_symbol argument/1)]]
+ ($_ _.and
+ (_.cover [/.function]
+ (let [function?' (: (-> Type Code (-> [(List Analysis) Analysis] Bit) Bit)
+ (function (_ function_type output_term ?)
+ (|> (do //phase.monad
+ [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+ output_term)
+ (//type.expecting function_type))]
+ (in (case analysis
+ {//analysis.#Function it}
+ (? it)
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))))
+ function? (: (-> Type Code Bit)
+ (function (_ function_type output_term)
+ (function?' function_type output_term (function.constant true))))
+ inferring? (: (-> Type Code Bit)
+ (function (_ :expected: term)
+ (|> (do //phase.monad
+ [[:actual: analysis] (|> (/.function ..analysis function/0 argument/0 archive.empty
+ term)
+ //type.inferring)]
+ (in (case analysis
+ {//analysis.#Function [actual_env actual_body]}
+ (type#= :expected: :actual:)
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))))]
+ (and (function? (-> input/0 output/0) term/0)
+ (function? (-> input/0 input/0) $argument/0)
+
+ (function? {.#Named name/0 (-> input/0 output/0)} term/0)
+
+ (function? (All (_ a) (-> a a)) $argument/0)
+ (function? (Ex (_ a) (-> a a)) $argument/0)
+ (function? (Ex (_ a) (-> input/0 a)) term/0)
+ (function? (Ex (_ a) (-> a a)) term/0)
+ (function? (Rec self (-> input/0 self)) $function/0)
+
+ (function? (type ((All (_ a) (-> a a)) output/0)) term/0)
+ (not (function? (type ((All (_ a) (-> a a)) output/1)) term/0))
+
+ (function? (type ((Ex (_ a) (-> a a)) output/0)) term/0)
+ (not (function? (type ((Ex (_ a) (-> a a)) output/1)) term/0))
+
+ (function?' (-> input/0 input/1 input/0) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/0)))
+ (function (_ [outer body])
+ (and (list.empty? outer)
+ (case body
+ {//analysis.#Function [inner body]}
+ (n.= 1 (list.size inner))
+
+ _
+ false))))
+ (function?' (-> input/0 input/1 input/1) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/1)))
+ (function (_ [outer body])
+ (and (list.empty? outer)
+ (case body
+ {//analysis.#Function [inner body]}
+ (n.= 0 (list.size inner))
+
+ _
+ false))))
+
+ (|> (do //phase.monad
+ [[@var :var:] (//type.check check.var)
+ _ (//type.check (check.check :var: (-> input/0 output/0)))
+ analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+ term/0)
+ (//type.expecting :var:))]
+ (in (case analysis
+ {//analysis.#Function [actual_env actual_body]}
+ true
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))
+
+ (inferring? (All (_ a) (-> a output/0)) term/0)
+ (inferring? (All (_ a) (-> a a)) $argument/0)
+ (inferring? (All (_ @0) (-> @0 @0 (And .Bit @0)))
+ (` ([(~ $function/1) (~ $argument/1)]
+ [("lux is" (~ $argument/0) (~ $argument/1))
+ (~ $argument/1)]))))))
+ (_.cover [/.cannot_analyse]
+ (|> (do //phase.monad
+ [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+ term/1)
+ (//type.expecting (-> input/0 output/0)))]
+ (in (case analysis
+ {//analysis.#Function [actual_env actual_body]}
+ true
+
+ _
+ false)))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.cannot_analyse)))))
+ )))
(def: .public test
Test
- (<| (_.context (symbol.module (symbol /._)))
- ($_ _.and
- ..abstraction
- ..apply
- )))
+ (<| (_.covering /._)
+ (do [! random.monad]
+ [lux $//type.random_state
+ .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]]
+ [input/0 term/0] $//inference.simple_parameter
+ [input/1 term/1] $//inference.simple_parameter
+ output/0 ($type.random 0)
+ module/0 (random.ascii/lower 1)]
+ ($_ _.and
+ ..test|function
+ (_.cover [/.apply]
+ (let [reification? (: (-> Type (List Code) Type Bit)
+ (function (_ :abstraction: terms :expected:)
+ (|> (do //phase.monad
+ [[:actual: analysis] (|> (/.apply ..analysis terms
+ :abstraction:
+ (//analysis.unit)
+ archive.empty
+ (' []))
+ //type.inferring)]
+ (in (and (check.subsumes? :expected: :actual:)
+ (case analysis
+ {//analysis.#Apply _}
+ true
+
+ _
+ false))))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (try.else false))))]
+ (and (reification? (-> input/0 input/1 output/0) (list term/0 term/1) output/0)
+ (reification? (-> input/0 input/1 output/0) (list term/0) (-> input/1 output/0))
+ (reification? (All (_ a) (-> a a)) (list term/0) input/0)
+ (reification? (All (_ a) (-> a a a)) (list term/0) (-> input/0 input/0))
+ (reification? (All (_ a) (-> input/0 a)) (list term/0) .Nothing)
+ (reification? (All (_ a b) (-> a b a)) (list term/0) (All (_ b) (-> b input/0)))
+ (reification? (Ex (_ a) (-> a input/0)) (list (` ("lux io error" ""))) input/0)
+ (reification? (Ex (_ a) (-> input/0 a)) (list term/0) .Any))))
+ (_.cover [/.cannot_apply]
+ (|> (do //phase.monad
+ [_ (|> (/.apply ..analysis (list term/1 term/0)
+ (-> input/0 input/1 output/0)
+ (//analysis.unit)
+ archive.empty
+ (' []))
+ (//type.expecting output/0))]
+ (in false))
+ (//module.with 0 module/0)
+ (//phase#each product.right)
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.cannot_apply)))))
+ ))))