aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/test
diff options
context:
space:
mode:
authorEduardo Julian2022-02-18 17:37:21 -0400
committerEduardo Julian2022-02-18 17:37:21 -0400
commite3986e8a7b9a997441477cdb333d3a8537dc49fb (patch)
treead3823d894f75dfbda2140242902239ade8775dd /stdlib/source/test
parent99361f07e4dd5724611e13a91ba8f14f039cdf0c (diff)
Yet more fixes for JVM interop.
Diffstat (limited to '')
-rw-r--r--stdlib/source/test/lux/control/parser/type.lux18
-rw-r--r--stdlib/source/test/lux/tool.lux4
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux822
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux4
-rw-r--r--stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux1
-rw-r--r--stdlib/source/test/lux/tool/compiler/meta/archive/module/document.lux2
6 files changed, 648 insertions, 203 deletions
diff --git a/stdlib/source/test/lux/control/parser/type.lux b/stdlib/source/test/lux/control/parser/type.lux
index 39656a32c..6476f9e30 100644
--- a/stdlib/source/test/lux/control/parser/type.lux
+++ b/stdlib/source/test/lux/control/parser/type.lux
@@ -6,6 +6,7 @@
[abstract
[monad {"+" do}]]
[control
+ [pipe {"+" case>}]
["[0]" try]
["[0]" exception]]
[data
@@ -150,6 +151,23 @@
/.parameter)
{.#Parameter 0})
(!expect {try.#Success [quantification##binding argument##binding _]})))
+ (_.cover [/.argument]
+ (let [argument? (: (-> Nat Nat Bit)
+ (function (_ @ expected)
+ (|> (/.result (<| (/.with_extension quantification)
+ (/.with_extension argument)
+ (/.with_extension quantification)
+ (/.with_extension argument)
+ (do //.monad
+ [env /.env
+ _ /.any]
+ (in (/.argument env @))))
+ not_parameter)
+ (!expect (^multi {try.#Success [_ _ _ _ actual]}
+ (n.= expected actual))))))]
+ (and (argument? 0 2)
+ (argument? 1 3)
+ (argument? 2 0))))
(_.cover [/.wrong_parameter]
(|> (/.result (<| (/.with_extension quantification)
(/.with_extension argument)
diff --git a/stdlib/source/test/lux/tool.lux b/stdlib/source/test/lux/tool.lux
index 07824362b..22267936f 100644
--- a/stdlib/source/test/lux/tool.lux
+++ b/stdlib/source/test/lux/tool.lux
@@ -18,7 +18,8 @@
["[1]/[0]" simple]
["[1]/[0]" complex]
["[1]/[0]" reference]
- ["[1]/[0]" function]]
+ ["[1]/[0]" function]
+ ["[1]/[0]" case]]
... ["[1]/[0]" synthesis]
]]]
["[1][0]" meta "_"
@@ -47,6 +48,7 @@
/phase/analysis/complex.test
/phase/analysis/reference.test
/phase/analysis/function.test
+ /phase/analysis/case.test
... /syntax.test
... /synthesis.test
))
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux
index c85e3896e..8ade96d8a 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/case.lux
@@ -1,210 +1,636 @@
(.using
+ [library
[lux "*"
- [abstract
- ["[0]" monad {"+" do}]]
- [data
- ["%" text/format {"+" format}]]
- ["r" math/random {"+" Random} ("[1]#[0]" monad)]
["_" test {"+" Test}]
+ [abstract
+ [monad {"+" do}]]
[control
- pipe
- ["[0]" maybe]]
+ [pipe {"+" case>}]
+ ["[0]" try {"+" Try} ("[1]#[0]" functor)]
+ ["[0]" exception]]
[data
["[0]" product]
- ["[0]" text ("[1]#[0]" equivalence)]
- [number
- ["n" nat]]
- [collection
- ["[0]" list ("[1]#[0]" monad)]
- ["[0]" set]]]
- ["[0]" type
- ["[0]" check]]
+ ["[0]" text
+ ["%" format]]]
[macro
["[0]" code]]
- [meta
- ["[0]" symbol]]]
- [//
- ["_[0]" primitive]
- ["_[0]" structure]]
- [\\
- ["[0]" /
- ["/[1]" //
- ["[1][0]" module]
- ["[1][0]" type]
- ["/[1]" // "_"
- ["/[1]" //
- ["[1][0]" analysis {"+" Analysis Variant Tag Operation}]
- [///
- ["[0]" phase]
- [meta
- ["[0]" archive]]]]]]]])
-
-(def: (exhaustive_weaving branchings)
- (-> (List (List Code)) (List (List Code)))
- (case branchings
- {.#End}
- {.#End}
-
- {.#Item head+ {.#End}}
- (list#each (|>> list) head+)
-
- {.#Item head+ tail++}
- (do list.monad
- [tail+ (exhaustive_weaving tail++)
- head head+]
- (in {.#Item head tail+}))))
-
-(def: .public (exhaustive_branches allow_literals? variantTC inputC)
- (-> Bit (List [Code Code]) Code (Random (List Code)))
- (case inputC
- [_ {.#Bit _}]
- (r#in (list (' #0) (' #1)))
-
- (^template [<tag> <gen> <wrapper>]
- [[_ {<tag> _}]
- (if allow_literals?
- (do [! r.monad]
- [?sample (r.maybe <gen>)]
- (case ?sample
- {.#Some sample}
- (do !
- [else (exhaustive_branches allow_literals? variantTC inputC)]
- (in (list& (<wrapper> sample) else)))
-
- {.#None}
- (in (list (' _)))))
- (r#in (list (' _))))])
- ([.#Nat r.nat code.nat]
- [.#Int r.int code.int]
- [.#Rev r.rev code.rev]
- [.#Frac r.frac code.frac]
- [.#Text (r.unicode 5) code.text])
-
- (^ [_ {.#Tuple (list)}])
- (r#in (list (' [])))
-
- [_ {.#Tuple members}]
- (do [! r.monad]
- [member_wise_patterns (monad.each ! (exhaustive_branches allow_literals? variantTC) members)]
- (in (|> member_wise_patterns
- exhaustive_weaving
- (list#each code.tuple))))
-
- (^ [_ {.#Record (list)}])
- (r#in (list (' {})))
-
- [_ {.#Record kvs}]
- (do [! r.monad]
- [.let [ks (list#each product.left kvs)
- vs (list#each product.right kvs)]
- member_wise_patterns (monad.each ! (exhaustive_branches allow_literals? variantTC) vs)]
- (in (|> member_wise_patterns
- exhaustive_weaving
- (list#each (|>> (list.zipped/2 ks) code.record)))))
-
- (^ [_ {.#Form (list [_ {.#Tag _}] _)}])
- (do [! r.monad]
- [bundles (monad.each !
- (function (_ [_tag _code])
- (do !
- [v_branches (exhaustive_branches allow_literals? variantTC _code)]
- (in (list#each (function (_ pattern) (` ((~ _tag) (~ pattern))))
- v_branches))))
- variantTC)]
- (in (list#conjoint bundles)))
-
- _
- (r#in (list))
- ))
-
-(def: .public (input variant_tags record_tags primitivesC)
- (-> (List Code) (List Code) (List Code) (Random Code))
- (r.rec
- (function (_ input)
- ($_ r.either
- (r#each product.right _primitive.primitive)
- (do [! r.monad]
- [choice (|> r.nat (# ! each (n.% (list.size variant_tags))))
- .let [choiceT (maybe.trusted (list.item choice variant_tags))
- choiceC (maybe.trusted (list.item choice primitivesC))]]
- (in (` ((~ choiceT) (~ choiceC)))))
- (do [! r.monad]
- [size (|> r.nat (# ! each (n.% 3)))
- elems (r.list size input)]
- (in (code.tuple elems)))
- (r#in (code.record (list.zipped/2 record_tags primitivesC)))
- ))))
-
-(def: (branch body pattern)
- (-> Code Code [Code Code])
- [pattern body])
+ [math
+ ["[0]" random]]
+ ["[0]" type ("[1]#[0]" equivalence)
+ ["[0]" check]]]]
+ [\\library
+ ["[0]" /
+ ["/[1]" //
+ [//
+ ["[1][0]" extension
+ ["[1]/[0]" analysis "_"
+ ["[1]" lux]]]
+ [//
+ ["[1][0]" analysis
+ [evaluation {"+" Eval}]
+ ["[2][0]" macro]
+ ["[2][0]" scope]
+ ["[2][0]" module]
+ ["[2][0]" coverage]
+ ["[2][0]" type
+ ["$[1]" \\test]]
+ ["[2][0]" inference "_"
+ ["$[1]" \\test]]]
+ [///
+ ["[1][0]" phase ("[1]#[0]" monad)]
+ [meta
+ ["[0]" archive]]]]]]]])
+
+(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|tuple
+ Test
+ (do [! random.monad]
+ [lux $//type.random_state
+ .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]]
+ module/0 (random.ascii/lower 1)
+ name/0 (# ! each (|>> [module/0]) (random.ascii/lower 2))
+ [input/0 simple/0] $//inference.simple_parameter
+ [input/1 simple/1] $//inference.simple_parameter
+ [input/2 simple/2] $//inference.simple_parameter
+ $binding/0 (# ! each code.local_symbol (random.ascii/lower 3))
+ $binding/1 (# ! each code.local_symbol (random.ascii/lower 4))
+ $binding/2 (# ! each code.local_symbol (random.ascii/lower 5))]
+ ($_ _.and
+ (_.cover [/.tuple]
+ (let [tuple? (: (-> Type Type Bit)
+ (function (_ :input: :expected:)
+ (and (|> :input:
+ /.tuple
+ (check.result check.fresh_context)
+ (try#each (|>> product.right (type#= :expected:)))
+ (try.else false))
+ (|> (do check.monad
+ [[@var :var:] check.var
+ _ (check.check :var: :input:)]
+ (/.tuple :var:))
+ (check.result check.fresh_context)
+ (try#each (|>> product.right (type#= :expected:)))
+ (try.else false)))))]
+ (and (tuple? input/0
+ (type.anonymous input/0))
+ (tuple? (Tuple input/0 input/1 input/2)
+ (Tuple input/0 input/1 input/2))
+ (tuple? {.#Named name/0 (Tuple input/0 input/1 input/2)}
+ (Tuple input/0 input/1 input/2))
+ (tuple? (All (_ a b c) (Tuple input/0 input/1 input/2))
+ (Tuple (All (_ a b c) input/0)
+ (All (_ a b c) input/1)
+ (All (_ a b c) input/2)))
+ (tuple? (type ((All (_ a b c) (Tuple a b c)) input/0 input/1 input/2))
+ (Tuple input/0 input/1 input/2))
+ (|> (do check.monad
+ [[@var :var:] check.var
+ _ (check.bind (All (_ a b c) (Tuple a b c)) @var)]
+ (/.tuple (type (:var: input/0 input/1 input/2))))
+ (check.result check.fresh_context)
+ (try#each (|>> product.right (type#= (Tuple input/0 input/1 input/2))))
+ (try.else false))
+ (|> (do check.monad
+ [[@0 :0:] check.existential
+ [@1 :1:] check.existential
+ [_ :tuple:] (/.tuple (Ex (_ a b c) (Tuple a input/1 c)))
+ context check.context
+ _ (check.with context)
+ _ (check.check (Tuple :0: input/1 :1:) :tuple:)
+ _ (check.with context)
+ _ (check.check :tuple: (Tuple :0: input/1 :1:))]
+ (in true))
+ (check.result check.fresh_context)
+ (try.else false)))))
+ (_.cover [/.non_tuple]
+ (and (|> (do check.monad
+ [[@var :var:] check.var
+ _ (/.tuple :var:)]
+ (in false))
+ (check.result check.fresh_context)
+ (exception.otherwise (text.contains? (value@ exception.#label /.non_tuple))))
+ (|> (do check.monad
+ [[@var :var:] check.var
+ _ (/.tuple (type (:var: input/0 input/1 input/2)))]
+ (in false))
+ (check.result check.fresh_context)
+ (exception.otherwise (text.contains? (value@ exception.#label /.non_tuple))))
+ (|> (do check.monad
+ [_ (/.tuple (type (input/0 input/1 input/2)))]
+ (in false))
+ (check.result check.fresh_context)
+ (exception.otherwise (text.contains? (value@ exception.#label /.non_tuple))))
+ (|> (do check.monad
+ [[@var :var:] check.var
+ _ (check.bind input/0 @var)
+ _ (/.tuple (type (:var: input/1 input/2)))]
+ (in false))
+ (check.result check.fresh_context)
+ (exception.otherwise (text.contains? (value@ exception.#label /.non_tuple))))))
+ )))
+
+(def: (test|case lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/2] [$binding/0 $binding/1 $binding/2] [output/0 body/0] [output/1 body/1] [bit/0 nat/0])
+ (-> Lux Symbol [Type Code] [Type Code] [Type Code] [Code Code Code] [Type Code] [Type Code] [Bit Nat] Bit)
+ (let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]
+ case? (: (-> Code (List [Code Code]) Bit)
+ (function (_ input branches)
+ (|> (do //phase.monad
+ [analysis (|> (/.case ..analysis branches archive.empty input)
+ (//type.expecting output/0))]
+ (in true))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (try.else false))))
+
+ body_types_mismatch!
+ (and (not (case? (code.bit bit/0) (list [(` #0) body/1]
+ [(` #1) body/1])))
+ (not (case? (code.bit bit/0) (list [(` #0) body/0]
+ [(` #1) body/1]))))
+
+ input_types_mismatch!
+ (and (not (case? (code.nat nat/0) (list [(` #0) body/0]
+ [(` #1) body/0])))
+ (not (case? (code.bit bit/0) (list [(code.nat nat/0) body/0]
+ [$binding/0 body/0]))))
+
+ handles_singletons!
+ (and (case? simple/0 (list [(` [(~ $binding/0)]) body/0]))
+ (case? simple/0 (list [(` [(~ simple/0)]) body/0]
+ [(` [(~ $binding/0)]) body/0]))
+ (case? (code.bit bit/0) (list [(` [#0]) body/0]
+ [(` [#1]) body/0])))
+
+ can_infer_body!
+ (|> (do //phase.monad
+ [[:actual: analysis] (|> (code.bit bit/0)
+ (/.case ..analysis
+ (list [(` #0) body/0]
+ [(` #1) body/0])
+ archive.empty)
+ //type.inferring)]
+ (in (type#= output/0 :actual:)))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (try.else false))
+
+ ensures_consistent_bodies!
+ (|> (do //phase.monad
+ [[:actual: analysis] (|> (code.bit bit/0)
+ (/.case ..analysis
+ (list [(` #0) body/0]
+ [(` #1) body/1])
+ archive.empty)
+ //type.inferring)]
+ (in false))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (try.else true))]
+ (and body_types_mismatch!
+ input_types_mismatch!
+ handles_singletons!
+ can_infer_body!
+ ensures_consistent_bodies!
+
+ (case? (` [])
+ (list [(` []) body/0]))
+ (case? (` [])
+ (list [$binding/0 body/0]))
+
+ (case? (code.bit bit/0) (list [(` #0) body/0]
+ [(` #1) body/0]))
+ (case? (code.bit bit/0) (list [(` #1) body/0]
+ [(` #0) body/0]))
+
+ (case? simple/0 (list [$binding/0 body/0]))
+ (case? simple/0 (list [simple/0 body/0]
+ [$binding/0 body/0]))
+
+ (case? (` [(~ simple/0) (~ simple/1) (~ simple/2)])
+ (list [$binding/0 body/0]))
+ (case? (` [(~ simple/0) (~ simple/1) (~ simple/2)])
+ (list [(` [(~ $binding/0) (~ $binding/1)]) body/0]))
+ (case? (` [(~ simple/0) (~ simple/1) (~ simple/2)])
+ (list [(` [(~ simple/0) (~ simple/1) (~ simple/2)]) body/0]
+ ... 000
+ [(` [(~ $binding/0) (~ simple/1) (~ simple/2)]) body/0]
+ ... 001
+ [(` [(~ simple/0) (~ $binding/1) (~ simple/2)]) body/0]
+ ... 010
+ [(` [(~ $binding/0) (~ $binding/1) (~ simple/2)]) body/0]
+ ... 011
+ [(` [(~ simple/0) (~ simple/1) (~ $binding/2)]) body/0]
+ ... 100
+ [(` [(~ $binding/0) (~ simple/1) (~ $binding/2)]) body/0]
+ ... 101
+ [(` [(~ simple/0) (~ $binding/1) (~ $binding/2)]) body/0]
+ ... 110
+ [(` [(~ $binding/0) (~ $binding/1) (~ $binding/2)]) body/0]
+ ... 111
+ )))))
+
+(def: (test|redundancy lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/2] [$binding/0 $binding/1 $binding/2] [output/0 body/0] bit/0)
+ (-> Lux Symbol [Type Code] [Type Code] [Type Code] [Code Code Code] [Type Code] Bit Bit)
+ (let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]
+ redundant? (: (-> Code (List [Code Code]) Bit)
+ (function (_ input branches)
+ (|> (do //phase.monad
+ [analysis (|> (/.case ..analysis branches archive.empty input)
+ (//type.expecting output/0))]
+ (in true))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label //coverage.redundancy))))))]
+ (and (redundant? (` [])
+ (list [(` []) body/0]
+ [(` []) body/0]))
+ (redundant? (` [])
+ (list [$binding/0 body/0]
+ [$binding/0 body/0]))
+ (redundant? (code.bit bit/0) (list [(` #0) body/0]
+ [(` #1) body/0]
+ [(` #0) body/0]))
+ (redundant? (code.bit bit/0) (list [(` #0) body/0]
+ [(` #1) body/0]
+ [(` #1) body/0]))
+ (redundant? (code.bit bit/0) (list [(` #0) body/0]
+ [(` #1) body/0]
+ [$binding/0 body/0]))
+ (redundant? simple/0 (list [$binding/0 body/0]
+ [$binding/0 body/0]))
+ (redundant? simple/0 (list [simple/0 body/0]
+ [$binding/0 body/0]
+ [$binding/0 body/0]))
+ (redundant? simple/0 (list [$binding/0 body/0]
+ [simple/0 body/0]))
+ (redundant? (` [(~ simple/0) (~ simple/1) (~ simple/2)])
+ (list [$binding/0 body/0]
+ [$binding/0 body/0]))
+ (redundant? (` [(~ simple/0) (~ simple/1) (~ simple/2)])
+ (list [(` [(~ $binding/0) (~ $binding/1)]) body/0]
+ [(` [(~ $binding/0) (~ $binding/1)]) body/0]))
+ (redundant? (` [(~ simple/0) (~ simple/1) (~ simple/2)])
+ (list [(` [(~ $binding/0) (~ $binding/1)]) body/0]
+ [$binding/0 body/0]))
+ (redundant? (` [(~ simple/0) (~ simple/1) (~ simple/2)])
+ (list [$binding/0 body/0]
+ [(` [(~ $binding/0) (~ $binding/1)]) body/0])))))
+
+(def: (test|variant lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/2] [$binding/0 $binding/1 $binding/2] [output/0 body/0] [output/1 body/1] [bit/0 nat/0])
+ (-> Lux Symbol [Type Code] [Type Code] [Type Code] [Code Code Code] [Type Code] [Type Code] [Bit Nat] Bit)
+ (let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]
+
+ tag/0 (%.code $binding/0)
+ tag/1 (%.code $binding/1)
+ tag/2 (%.code $binding/2)
+
+ tags/* (list tag/0 tag/1 tag/2)
+ :variant: {.#Named [module/0 name/0] (type.variant (list input/0 input/1 input/2))}
+
+ tag/0 (code.symbol [module/0 tag/0])
+ tag/1 (code.symbol [module/0 tag/1])
+ tag/2 (code.symbol [module/0 tag/2])
+
+ variant? (: (-> Code (List [Code Code]) Bit)
+ (function (_ input branches)
+ (|> (do //phase.monad
+ [_ (//module.declare_labels false tags/* false :variant:)
+ analysis (|> (/.case ..analysis branches archive.empty input)
+ (//type.expecting output/0))]
+ (in true))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (try.else false))))
+
+ can_bind!
+ (and (variant? (` {(~ tag/0) (~ simple/0)})
+ (list [$binding/0 body/0]))
+ (variant? (` {(~ tag/1) (~ simple/1)})
+ (list [$binding/0 body/0]))
+ (variant? (` {(~ tag/2) (~ simple/2)})
+ (list [$binding/0 body/0])))
+
+ can_bind_variant!
+ (variant? (` {(~ tag/0) (~ simple/0)})
+ (list [(` {(~ tag/0) (~ $binding/0)}) body/0]
+ [(` {(~ tag/1) (~ $binding/1)}) body/0]
+ [(` {(~ tag/2) (~ $binding/2)}) body/0]))
+
+ can_bind_sum!
+ (variant? (` {(~ tag/0) (~ simple/0)})
+ (list [(` {0 #0 (~ $binding/0)}) body/0]
+ [(` {1 #0 (~ $binding/1)}) body/0]
+ [(` {1 #1 (~ $binding/2)}) body/0]))
+
+ can_check_exhaustiveness!
+ (variant? (` {(~ tag/0) (~ simple/0)})
+ (list [(` {(~ tag/0) (~ simple/0)}) body/0]
+ [(` {(~ tag/0) (~ $binding/0)}) body/0]
+
+ [(` {(~ tag/1) (~ simple/1)}) body/0]
+ [(` {(~ tag/1) (~ $binding/1)}) body/0]
+
+ [(` {(~ tag/2) (~ simple/2)}) body/0]
+ [(` {(~ tag/2) (~ $binding/2)}) body/0]))
+
+ can_bind_partial_variant!
+ (variant? (` {(~ tag/0) (~ simple/0)})
+ (list [(` {(~ tag/0) (~ $binding/0)}) body/0]
+ [(` {0 #1 (~ $binding/1)}) body/0]))]
+ (and can_bind!
+ can_bind_variant!
+ can_bind_sum!
+ can_check_exhaustiveness!
+ can_bind_partial_variant!
+ )))
+
+(def: (test|record lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/2] [$binding/0 $binding/1 $binding/2] [output/0 body/0] [output/1 body/1] [bit/0 nat/0])
+ (-> Lux Symbol [Type Code] [Type Code] [Type Code] [Code Code Code] [Type Code] [Type Code] [Bit Nat] Bit)
+ (let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]
+
+ slot/0 (%.code $binding/0)
+ slot/1 (%.code $binding/1)
+ slot/2 (%.code $binding/2)
+
+ slots/* (list slot/0 slot/1 slot/2)
+ :record: {.#Named [module/0 name/0] (type.tuple (list input/0 input/1 input/2))}
+
+ slot/0 (code.symbol [module/0 slot/0])
+ slot/1 (code.symbol [module/0 slot/1])
+ slot/2 (code.symbol [module/0 slot/2])
+
+ record? (: (-> Code (List [Code Code]) Bit)
+ (function (_ input branches)
+ (|> (do //phase.monad
+ [_ (//module.declare_labels true slots/* false :record:)
+ analysis (|> (/.case ..analysis branches archive.empty input)
+ (//type.expecting output/0))]
+ (in true))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (try.else false))))
+
+ can_bind!
+ (record? (` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)])
+ (list [$binding/0 body/0]))
+
+ can_bind_record!
+ (record? (` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)])
+ (list [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ $binding/2)]) body/0]))
+
+ can_bind_tuple!
+ (record? (` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)])
+ (list [(` [(~ $binding/0) (~ $binding/1) (~ $binding/2)]) body/0]))
+
+ can_deduce_record!
+ (record? (` [(~ simple/0)
+ (~ simple/1)
+ (~ simple/2)])
+ (list [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ $binding/2)]) body/0]))
+
+ can_check_exhaustiveness!
+ (record? (` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)])
+ (list [(` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)]) body/0]
+ ... 000
+ [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)]) body/0]
+ ... 001
+ [(` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ simple/2)]) body/0]
+ ... 010
+ [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ simple/2)]) body/0]
+ ... 011
+ [(` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ $binding/2)]) body/0]
+ ... 100
+ [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ $binding/2)]) body/0]
+ ... 101
+ [(` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ $binding/2)]) body/0]
+ ... 110
+ [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ $binding/2)]) body/0]
+ ... 111
+ ))
+
+ cannot_repeat_slot!
+ (not (record? (` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)])
+ (list [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ $binding/2)
+ (~ slot/2) (~ $binding/2)]) body/0])))
+
+ cannot_omit_slot!
+ (not (record? (` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)])
+ (list [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ $binding/1)]) body/0])))
+
+ can_bind_partial_tuple!
+ (record? (` [(~ slot/0) (~ simple/0)
+ (~ slot/1) (~ simple/1)
+ (~ slot/2) (~ simple/2)])
+ (list [(` [(~ $binding/0) (~ $binding/1)]) body/0]))]
+ (and can_bind!
+ can_bind_record!
+ can_bind_tuple!
+ can_deduce_record!
+ can_check_exhaustiveness!
+ cannot_repeat_slot!
+ cannot_omit_slot!
+ can_bind_partial_tuple!)))
(def: .public test
- (<| (_.context (symbol.module (symbol /._)))
- (do [! r.monad]
- [module_name (r.unicode 5)
- variant_name (r.unicode 5)
- record_name (|> (r.unicode 5) (r.only (|>> (text#= variant_name) not)))
- size (|> r.nat (# ! each (|>> (n.% 10) (n.max 2))))
- variant_tags (|> (r.set text.hash size (r.unicode 5)) (# ! each set.list))
- record_tags (|> (r.set text.hash size (r.unicode 5)) (# ! each set.list))
- primitivesTC (r.list size _primitive.primitive)
- .let [primitivesT (list#each product.left primitivesTC)
- primitivesC (list#each product.right primitivesTC)
- code_tag (|>> [module_name] code.tag)
- variant_tags+ (list#each code_tag variant_tags)
- record_tags+ (list#each code_tag record_tags)
- variantTC (list.zipped/2 variant_tags+ primitivesC)]
- inputC (input variant_tags+ record_tags+ primitivesC)
- [outputT outputC] (r.only (|>> product.left (same? Any) not)
- _primitive.primitive)
- .let [analyse_pm (function (_ branches)
- (|> (/.case _primitive.phase branches archive.empty inputC)
- (//type.with_type outputT)
- ////analysis.with_scope
- (do phase.monad
- [_ (//module.declare_tags variant_tags false
- {.#Named [module_name variant_name]
- (type.variant primitivesT)})
- _ (//module.declare_tags record_tags false
- {.#Named [module_name record_name]
- (type.tuple primitivesT)})])
- (//module.with_module 0 module_name)))]
- exhaustive_patterns (exhaustive_branches true variantTC inputC)
- .let [exhaustive_branchesC (list#each (branch outputC)
- exhaustive_patterns)]]
+ Test
+ (<| (_.covering /._)
+ (do [! random.monad]
+ [lux $//type.random_state
+ .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+ //extension.#state lux]]
+ module/0 (random.ascii/lower 1)
+ name/0 (random.ascii/lower 2)
+ [input/0 simple/0] $//inference.simple_parameter
+ [input/1 simple/1] $//inference.simple_parameter
+ [input/2 simple/2] $//inference.simple_parameter
+ [output/0 body/0] $//inference.simple_parameter
+ [output/1 body/1] (random.only (|>> product.left (same? output/0) not)
+ $//inference.simple_parameter)
+ $binding/0 (# ! each code.local_symbol (random.ascii/lower 3))
+ $binding/1 (# ! each code.local_symbol (random.ascii/lower 4))
+ $binding/2 (# ! each code.local_symbol (random.ascii/lower 5))
+ extension/0 (# ! each code.text (random.ascii/lower 6))
+ bit/0 random.bit
+ nat/0 random.nat]
($_ _.and
- (_.test "Will reject empty pattern-matching (no branches)."
- (|> (analyse_pm (list))
- _structure.check_fails))
- (_.test "Can analyse exhaustive pattern-matching."
- (|> (analyse_pm exhaustive_branchesC)
- _structure.check_succeeds))
- (let [non_exhaustive_branchesC (list.first (-- (list.size exhaustive_branchesC))
- exhaustive_branchesC)]
- (_.test "Will reject non-exhaustive pattern-matching."
- (|> (analyse_pm non_exhaustive_branchesC)
- _structure.check_fails)))
- (do !
- [redundant_patterns (exhaustive_branches false variantTC inputC)
- redundancy_idx (|> r.nat (# ! each (n.% (list.size redundant_patterns))))
- .let [redundant_branchesC (<| (list!each (branch outputC))
- list.together
- (list (list.first redundancy_idx redundant_patterns)
- (list (maybe.trusted (list.item redundancy_idx redundant_patterns)))
- (list.after redundancy_idx redundant_patterns)))]]
- (_.test "Will reject redundant pattern-matching."
- (|> (analyse_pm redundant_branchesC)
- _structure.check_fails)))
- (do !
- [[heterogeneousT heterogeneousC] (r.only (|>> product.left (check.subsumes? outputT) not)
- _primitive.primitive)
- heterogeneous_idx (|> r.nat (# ! each (n.% (list.size exhaustive_patterns))))
- .let [heterogeneous_branchesC (list.together (list (list.first heterogeneous_idx exhaustive_branchesC)
- (list (let [[_pattern _body] (maybe.trusted (list.item heterogeneous_idx exhaustive_branchesC))]
- [_pattern heterogeneousC]))
- (list.after (++ heterogeneous_idx) exhaustive_branchesC)))]]
- (_.test "Will reject pattern-matching if the bodies of the branches do not all have the same type."
- (|> (analyse_pm heterogeneous_branchesC)
- _structure.check_fails)))
+ (_.cover [/.case]
+ (and (test|case lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/2] [$binding/0 $binding/1 $binding/2] [output/0 body/0] [output/1 body/1] [bit/0 nat/0])
+ (test|redundancy lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/1] [$binding/0 $binding/1 $binding/2] [output/0 body/0] [bit/0])
+ (test|variant lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/2] [$binding/0 $binding/1 $binding/2] [output/0 body/0] [output/1 body/1] [bit/0 nat/0])
+ (test|record lux [module/0 name/0] [input/0 simple/0] [input/1 simple/1] [input/2 simple/2] [$binding/0 $binding/1 $binding/2] [output/0 body/0] [output/1 body/1] [bit/0 nat/0])))
+ (_.cover [/.empty_branches]
+ (|> (do //phase.monad
+ [analysis (|> (/.case ..analysis (list) archive.empty simple/0)
+ (//type.expecting output/0))]
+ (in false))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.empty_branches)))))
+ (_.cover [/.non_exhaustive]
+ (let [non_exhaustive? (: (-> (List [Code Code]) Bit)
+ (function (_ branches)
+ (|> (do //phase.monad
+ [analysis (|> (/.case ..analysis branches archive.empty simple/0)
+ (//type.expecting output/0))]
+ (in false))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.non_exhaustive))))))]
+ (and (non_exhaustive? (list [simple/0 body/0]))
+ (not (non_exhaustive? (list [simple/0 body/0]
+ [$binding/0 body/0]))))))
+ (_.cover [/.invalid]
+ (let [invalid? (: (-> (List [Code Code]) Bit)
+ (function (_ branches)
+ (|> (do //phase.monad
+ [analysis (|> (/.case ..analysis branches archive.empty simple/0)
+ (//type.expecting output/0))]
+ (in false))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.invalid))))))]
+ (and (invalid? (list [(` ((~ extension/0) (~ $binding/0) (~ $binding/1) (~ $binding/2)))
+ body/0]))
+ (invalid? (list [(` {(~ extension/0) (~ $binding/0) (~ $binding/1) (~ $binding/2)})
+ body/0]))
+ (invalid? (list [(` {[] (~ $binding/0) (~ $binding/1) (~ $binding/2)})
+ body/0])))))
+ (_.cover [/.sum_has_no_case]
+ (let [tag/0 (%.code $binding/0)
+ tag/1 (%.code $binding/1)
+ tag/2 (%.code $binding/2)
+
+ tags/* (list tag/0 tag/1 tag/2)
+ :variant: {.#Named [module/0 name/0] (type.variant (list input/0 input/1 input/2))}
+
+ tag/0 (code.symbol [module/0 tag/0])
+ tag/1 (code.symbol [module/0 tag/1])
+ tag/2 (code.symbol [module/0 tag/2])]
+ (|> (do //phase.monad
+ [_ (//module.declare_labels false tags/* false :variant:)
+ analysis (|> (` {(~ tag/0) (~ simple/0)})
+ (/.case ..analysis
+ (list [(` {0 #0 (~ $binding/0)}) body/0]
+ [(` {1 #0 (~ $binding/1)}) body/0]
+ [(` {2 #0 (~ $binding/2)}) body/0]
+ [(` {2 #1 (~ $binding/2)}) body/0])
+ archive.empty)
+ (//type.expecting output/0))]
+ (in false))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.sum_has_no_case))))))
+ (_.cover [/.mismatch]
+ (let [slot/0 (%.code $binding/0)
+ slot/1 (%.code $binding/1)
+ slot/2 (%.code $binding/2)
+
+ slots/* (list slot/0 slot/1 slot/2)
+ :record: {.#Named [module/0 name/0] (type.tuple (list input/0 input/1 input/2))}
+
+ slot/0 (code.symbol [module/0 slot/0])
+ slot/1 (code.symbol [module/0 slot/1])
+ slot/2 (code.symbol [module/0 slot/2])]
+ (and (|> (do //phase.monad
+ [analysis (|> (` (~ simple/0))
+ (/.case ..analysis
+ (list [(` {0 #0 (~ $binding/0)}) body/0]
+ [(` {1 #0 (~ $binding/1)}) body/0]
+ [(` {1 #1 (~ $binding/2)}) body/0])
+ archive.empty)
+ (//type.expecting output/0))]
+ (in false))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.mismatch))))
+ (|> (do //phase.monad
+ [_ (//module.declare_labels true slots/* false :record:)
+ analysis (|> (` (~ simple/0))
+ (/.case ..analysis
+ (list [(` [(~ slot/0) (~ $binding/0)
+ (~ slot/1) (~ $binding/1)
+ (~ slot/2) (~ $binding/2)]) body/0])
+ archive.empty)
+ (//type.expecting output/0))]
+ (in false))
+ //scope.with
+ (//module.with 0 module/0)
+ (//phase#each (|>> product.right product.right))
+ (//phase.result state)
+ (exception.otherwise (text.contains? (value@ exception.#label /.mismatch)))))))
+
+ ..test|tuple
))))
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 ed111c5e4..21813bb01 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
@@ -471,7 +471,7 @@
(function (_ expected input)
(|> (do //phase.monad
[_ (//module.declare_labels true slots/0 false :record:)]
- (/.normal input))
+ (/.normal false input))
(//module.with 0 module)
(//phase#each product.right)
(//phase.result state)
@@ -484,7 +484,7 @@
(and (normal? (list) (list))
(normal? expected_record global_record)
(normal? expected_record local_record)
- (|> (/.normal tuple)
+ (|> (/.normal false tuple)
(//phase.result state)
(case> {try.#Success {.#None}}
true
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 b5f2e4fc4..a5f5953e6 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
@@ -38,7 +38,6 @@
["[1][0]" analysis {"+" Analysis}
[evaluation {"+" Eval}]
["[2][0]" macro]
- ["[2][0]" scope]
["[2][0]" module]
["[2][0]" type
["$[1]" \\test]]
diff --git a/stdlib/source/test/lux/tool/compiler/meta/archive/module/document.lux b/stdlib/source/test/lux/tool/compiler/meta/archive/module/document.lux
index a73bf751d..a99e8eccf 100644
--- a/stdlib/source/test/lux/tool/compiler/meta/archive/module/document.lux
+++ b/stdlib/source/test/lux/tool/compiler/meta/archive/module/document.lux
@@ -80,7 +80,7 @@
(|> expected
(/.document key/0)
(binaryF.result (/.writer binaryF.nat))
- (<binary>.result (/.parser <binary>.nat))
+ (<binary>.result (/.parser key/0 <binary>.nat))
(case> {try.#Success it}
(and (/signature#= signature/0 (/.signature it))
(|> it