aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc
diff options
context:
space:
mode:
Diffstat (limited to 'new-luxc/source/luxc')
-rw-r--r--new-luxc/source/luxc/analyser/case.lux4
-rw-r--r--new-luxc/source/luxc/analyser/case/coverage.lux52
2 files changed, 28 insertions, 28 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))))