aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--new-luxc/source/luxc/analyser/case.lux4
-rw-r--r--new-luxc/source/luxc/analyser/case/coverage.lux52
-rw-r--r--new-luxc/test/test/luxc/analyser/case.lux46
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