diff options
| -rw-r--r-- | new-luxc/source/luxc/analyser/case.lux | 4 | ||||
| -rw-r--r-- | new-luxc/source/luxc/analyser/case/coverage.lux | 52 | ||||
| -rw-r--r-- | new-luxc/test/test/luxc/analyser/case.lux | 46 |
3 files changed, 51 insertions, 51 deletions
diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux index 0f5b4da4e..8ef4b030b 100644 --- a/new-luxc/source/luxc/analyser/case.lux +++ b/new-luxc/source/luxc/analyser/case.lux @@ -234,9 +234,9 @@ (|> outputH product;left &&coverage;determine) (L/map (|>. product;left &&coverage;determine) outputT)) (#R;Success coverage) - (if (&&coverage;total? coverage) + (if (&&coverage;exhaustive? coverage) (wrap []) - (&;fail "Pattern-matching is not total.")) + (&;fail "Pattern-matching is not exhaustive.")) (#R;Error error) (&;fail error))] diff --git a/new-luxc/source/luxc/analyser/case/coverage.lux b/new-luxc/source/luxc/analyser/case/coverage.lux index cb7341d7a..94aa06e9b 100644 --- a/new-luxc/source/luxc/analyser/case/coverage.lux +++ b/new-luxc/source/luxc/analyser/case/coverage.lux @@ -12,7 +12,7 @@ ## The coverage of a pattern-matching expression summarizes how well ## all the possible values of an input are being covered by the ## different patterns involved. -## Ideally, the pattern-matching has "total" coverage, which just +## Ideally, the pattern-matching has "exhaustive" coverage, which just ## means that every possible value can be matched by at least 1 ## pattern. ## Every other coverage is considered partial, and it would be valued @@ -27,12 +27,12 @@ (#Variant Nat (D;Dict Nat Coverage)) (#Seq Coverage Coverage) (#Alt Coverage Coverage) - #Total) + #Exhaustive) -(def: #export (total? coverage) +(def: #export (exhaustive? coverage) (-> Coverage Bool) (case coverage - (#Total _) + (#Exhaustive _) true _ @@ -41,12 +41,12 @@ (def: #export (determine pattern) (-> la;Pattern Coverage) (case pattern - ## Binding amounts to total coverage because any value can be + ## Binding amounts to exhaustive coverage because any value can be ## matched that way. - ## Unit [] amounts to total coverage because there is only one + ## Unit [] amounts to exhaustive coverage because there is only one ## possible value, so matching against it covers all cases. (^or (#la;BindP _) (^ (#la;TupleP (list)))) - #Total + #Exhaustive (^ (#la;TupleP (list singleton))) (determine singleton) @@ -59,27 +59,27 @@ ## Bools are the exception, since there is only "true" and ## "false", which means it is possible for boolean - ## pattern-matching to become total if complementary parts meet. + ## pattern-matching to become exhaustive if complementary parts meet. (#la;BoolP value) (#Bool value) - ## Tuple patterns can be total if there is totality for all of + ## Tuple patterns can be exhaustive if there is exhaustiveness for all of ## their sub-patterns. (#la;TupleP subs) (loop [subs subs] (case subs #;Nil - #Total + #Exhaustive (#;Cons sub subs') (let [post (recur subs')] - (if (total? post) + (if (exhaustive? post) (determine sub) (#Seq (determine sub) post))))) - ## Variant patterns can be shown to be total if all the possible - ## cases are handled totally. + ## Variant patterns can be shown to be exhaustive if all the possible + ## cases are handled exhaustively. (#la;VariantP tag-id num-tags sub) (#Variant num-tags (|> (D;new number;Hash<Nat>) @@ -91,7 +91,7 @@ (and (not left) right))) ## The coverage checker not only verifies that pattern-matching is -## total, but also that there are no redundant patterns. +## exhaustive, but also that there are no redundant patterns. ## Redundant patterns will never be executed, since there will ## always be a pattern prior to them that would match the input. ## Because of that, the presence of redundant patterns is assumed to @@ -112,7 +112,7 @@ (struct: _ (Eq Coverage) (def: (= reference sample) (case [reference sample] - [#Total #Total] + [#Exhaustive #Exhaustive] true [(#Bool sideR) (#Bool sideS)] @@ -141,26 +141,26 @@ ## After determining the coverage of each individual pattern, it is ## necessary to merge them all to figure out if the entire -## pattern-matching expression is total and whether it contains +## pattern-matching expression is exhaustive and whether it contains ## redundant patterns. (def: #export (merge addition so-far) (-> Coverage Coverage (R;Result Coverage)) (case [addition so-far] ## The addition cannot possibly improve the coverage. - [_ #Total] + [_ #Exhaustive] redundant-pattern ## The addition completes the coverage. - [#Total _] - (R/wrap #Total) + [#Exhaustive _] + (R/wrap #Exhaustive) [#Partial #Partial] (R/wrap #Partial) - ## 2 boolean coverages are total if they compliment one another. + ## 2 boolean coverages are exhaustive if they compliment one another. (^multi [(#Bool sideA) (#Bool sideSF)] (xor sideA sideSF)) - (R/wrap #Total) + (R/wrap #Exhaustive) [(#Variant allA casesA) (#Variant allSF casesSF)] (cond (not (n.= allSF allA)) @@ -184,8 +184,8 @@ casesSF (D;entries casesA))] (wrap (if (let [case-coverages (D;values casesM)] (and (n.= allSF (list;size case-coverages)) - (list;every? total? case-coverages))) - #Total + (list;every? exhaustive? case-coverages))) + #Exhaustive (#Variant allSF casesM))))) [(#Seq leftA rightA) (#Seq leftSF rightSF)] @@ -202,10 +202,10 @@ [true false] (do R;Monad<Result> [rightM (merge rightA rightSF)] - (if (total? rightM) - ## If all that follows is total, then it can be safely dropped + (if (exhaustive? rightM) + ## If all that follows is exhaustive, then it can be safely dropped ## (since only the "left" part would influence whether the - ## merged coverage is total or not). + ## merged coverage is exhaustive or not). (wrap leftSF) (wrap (#Seq leftSF rightM)))) diff --git a/new-luxc/test/test/luxc/analyser/case.lux b/new-luxc/test/test/luxc/analyser/case.lux index 69ab4cd99..3c05f5dad 100644 --- a/new-luxc/test/test/luxc/analyser/case.lux +++ b/new-luxc/test/test/luxc/analyser/case.lux @@ -25,7 +25,7 @@ (.. common) (test/luxc common)) -(def: (total-weaving branchings) +(def: (exhaustive-weaving branchings) (-> (List (List Code)) (List (List Code))) (case branchings #;Nil @@ -36,11 +36,11 @@ (#;Cons head+ tail++) (do list;Monad<List> - [tail+ (total-weaving tail++) + [tail+ (exhaustive-weaving tail++) head head+] (wrap (#;Cons head tail+))))) -(def: (total-branches-for allow-literals? variantTC inputC) +(def: (exhaustive-branches-for allow-literals? variantTC inputC) (-> Bool (List [Code Code]) Code (r;Random (List Code))) (case inputC [_ (#;Bool _)] @@ -54,7 +54,7 @@ (case ?sample (#;Some sample) (do @ - [else (total-branches-for allow-literals? variantTC inputC)] + [else (exhaustive-branches-for allow-literals? variantTC inputC)] (wrap (list& (<wrapper> sample) else))) #;None @@ -74,18 +74,18 @@ [_ (#;Tuple members)] (do r;Monad<Random> - [member-wise-patterns (monad;map @ (total-branches-for allow-literals? variantTC) members)] + [member-wise-patterns (monad;map @ (exhaustive-branches-for allow-literals? variantTC) members)] (wrap (|> member-wise-patterns - total-weaving + exhaustive-weaving (L/map code;tuple)))) [_ (#;Record kvs)] (do r;Monad<Random> [#let [ks (L/map product;left kvs) vs (L/map product;right kvs)] - member-wise-patterns (monad;map @ (total-branches-for allow-literals? variantTC) vs)] + member-wise-patterns (monad;map @ (exhaustive-branches-for allow-literals? variantTC) vs)] (wrap (|> member-wise-patterns - total-weaving + exhaustive-weaving (L/map (|>. (list;zip2 ks) code;record))))) (^ [_ (#;Form (list [_ (#;Tag _)] _))]) @@ -93,7 +93,7 @@ [bundles (monad;map @ (function [[_tag _code]] (do @ - [v-branches (total-branches-for allow-literals? variantTC _code)] + [v-branches (exhaustive-branches-for allow-literals? variantTC _code)] (wrap (L/map (function [pattern] (` ((~ _tag) (~ pattern)))) v-branches)))) variantTC)] @@ -145,23 +145,23 @@ [outputT outputC] gen-primitive [heterogeneousT heterogeneousC] (|> gen-primitive (r;filter (|>. product;left (tc;checks? outputT) not))) - total-patterns (total-branches-for true variantTC inputC) - redundant-patterns (total-branches-for false variantTC inputC) + exhaustive-patterns (exhaustive-branches-for true variantTC inputC) + redundant-patterns (exhaustive-branches-for false variantTC inputC) redundancy-idx (|> r;nat (:: @ map (n.% (list;size redundant-patterns)))) - heterogeneous-idx (|> r;nat (:: @ map (n.% (list;size total-patterns)))) - #let [total-branchesC (L/map (branch outputC) - total-patterns) - non-total-branchesC (list;take (n.dec (list;size total-branchesC)) - total-branchesC) + heterogeneous-idx (|> r;nat (:: @ map (n.% (list;size exhaustive-patterns)))) + #let [exhaustive-branchesC (L/map (branch outputC) + exhaustive-patterns) + non-exhaustive-branchesC (list;take (n.dec (list;size exhaustive-branchesC)) + exhaustive-branchesC) redundant-branchesC (<| (L/map (branch outputC)) list;concat (list (list;take redundancy-idx redundant-patterns) (list (assume (list;nth redundancy-idx redundant-patterns))) (list;drop redundancy-idx redundant-patterns))) - heterogeneous-branchesC (list;concat (list (list;take heterogeneous-idx total-branchesC) - (list (let [[_pattern _body] (assume (list;nth heterogeneous-idx total-branchesC))] + heterogeneous-branchesC (list;concat (list (list;take heterogeneous-idx exhaustive-branchesC) + (list (let [[_pattern _body] (assume (list;nth heterogeneous-idx exhaustive-branchesC))] [_pattern heterogeneousC])) - (list;drop (n.inc heterogeneous-idx) total-branchesC))) + (list;drop (n.inc heterogeneous-idx) exhaustive-branchesC))) ]] ($_ seq (test "Will reject empty pattern-matching (no branches)." @@ -169,7 +169,7 @@ (&;with-expected-type outputT (@;analyse-case analyse inputC (list)))) check-failure)) - (test "Can analyse total pattern-matching." + (test "Can analyse exhaustive pattern-matching." (|> (@module;with-module +0 module-name (do Monad<Lux> [_ (@module;declare-tags variant-tags false @@ -180,9 +180,9 @@ (type;tuple primitivesT)))] (&;with-scope (&;with-expected-type outputT - (@;analyse-case analyse inputC total-branchesC))))) + (@;analyse-case analyse inputC exhaustive-branchesC))))) check-success)) - (test "Will reject non-total pattern-matching." + (test "Will reject non-exhaustive pattern-matching." (|> (@module;with-module +0 module-name (do Monad<Lux> [_ (@module;declare-tags variant-tags false @@ -193,7 +193,7 @@ (type;tuple primitivesT)))] (&;with-scope (&;with-expected-type outputT - (@;analyse-case analyse inputC non-total-branchesC))))) + (@;analyse-case analyse inputC non-exhaustive-branchesC))))) check-failure)) (test "Will reject redundant pattern-matching." (|> (@module;with-module +0 module-name |