11 KiB
scratch/main> builtins.merge
Basics
non-exhaustive patterns
unique type T = A | B | C
test : T -> ()
test = cases
A -> ()
unique type T = A | B
test : (T, Optional T) -> ()
test = cases
(A, Some _) -> ()
(A, None) -> ()
(B, Some A) -> ()
(B, None) -> ()
redundant patterns
unique type T = A | B | C
test : T -> ()
test = cases
A -> ()
B -> ()
C -> ()
_ -> ()
unique type T = A | B
test : (T, Optional T) -> ()
test = cases
(A, Some _) -> ()
(A, None) -> ()
(B, Some _) -> ()
(B, None) -> ()
(A, Some A) -> ()
Uninhabited patterns
match is complete without covering uninhabited patterns
unique type V =
test : Optional (Optional V) -> ()
test = cases
None -> ()
Some None -> ()
uninhabited patterns are reported as redundant
unique type V =
test0 : V -> ()
test0 = cases
_ -> ()
unique type V =
test : Optional (Optional V) -> ()
test = cases
None -> ()
Some None -> ()
Some _ -> ()
Guards
Incomplete patterns due to guards should be reported
test : () -> ()
test = cases
() | false -> ()
test : Optional Nat -> Nat
test = cases
None -> 0
Some x
| isEven x -> x
Complete patterns with guards should be accepted
test : Optional Nat -> Nat
test = cases
None -> 0
Some x
| isEven x -> x
| otherwise -> 0
Pattern instantiation depth
Uncovered patterns are only instantiated as deeply as necessary to distinguish them from existing patterns.
unique type T = A | B | C
test : Optional (Optional T) -> ()
test = cases
None -> ()
Some None -> ()
unique type T = A | B | C
test : Optional (Optional T) -> ()
test = cases
None -> ()
Some None -> ()
Some (Some A) -> ()
Literals
Non-exhaustive
Nat
test : Nat -> ()
test = cases
0 -> ()
Boolean
test : Boolean -> ()
test = cases
true -> ()
Exhaustive
Nat
test : Nat -> ()
test = cases
0 -> ()
_ -> ()
Boolean
test : Boolean -> ()
test = cases
true -> ()
false -> ()
Redundant
Nat
test : Nat -> ()
test = cases
0 -> ()
0 -> ()
_ -> ()
Boolean
test : Boolean -> ()
test = cases
true -> ()
false -> ()
_ -> ()
Sequences
Exhaustive
test : [()] -> ()
test = cases
[] -> ()
x +: xs -> ()
Non-exhaustive
test : [()] -> ()
test = cases
[] -> ()
test : [()] -> ()
test = cases
x +: xs -> ()
test : [()] -> ()
test = cases
xs :+ x -> ()
test : [()] -> ()
test = cases
x0 +: (x1 +: xs) -> ()
[] -> ()
test : [()] -> ()
test = cases
[] -> ()
x0 +: [] -> ()
Uninhabited
Cons is not expected since V is uninhabited
unique type V =
test : [V] -> ()
test = cases
[] -> ()
Length restrictions can equate cons and nil patterns
Here the first pattern matches lists of length two or greater, the
second pattern matches lists of length 0. The third case matches when the
final element is false, while the fourth pattern matches when the
first element is true. However, the only possible list length at
the third or fourth clause is 1, so the first and final element must
be equal. Thus, the pattern match is exhaustive.
test : [Boolean] -> ()
test = cases
[a, b] ++ xs -> ()
[] -> ()
xs :+ false -> ()
true +: xs -> ()
This is the same idea as above but shows that fourth match is redundant.
test : [Boolean] -> ()
test = cases
[a, b] ++ xs -> ()
[] -> ()
xs :+ true -> ()
true +: xs -> ()
_ -> ()
This is another similar example. The first pattern matches lists of
length 5 or greater. The second matches lists of length 4 or greater where the
first and third element are true. The third matches lists of length 4
or greater where the final 4 elements are true, false, true, false.
The list must be exactly of length 4 to arrive at the second or third
clause, so the third pattern is redundant.
test : [Boolean] -> ()
test = cases
[a, b, c, d, f] ++ xs -> ()
[true, _, true, _] ++ _ -> ()
_ ++ [true, false, true, false] -> ()
_ -> ()
bugfix: Sufficient data decl map
unique type T = A
unit2t : Unit -> T
unit2t = cases
() -> A
scratch/main> add
Pattern coverage checking needs the data decl map to contain all transitive type dependencies of the scrutinee type. We do this before typechecking begins in a roundabout way: fetching all transitive type dependencies of references that appear in the expression.
This test ensures that we have fetched the T type although there is
no data decl reference to T in witht.
witht : Unit
witht = match unit2t () with
x -> ()
unique type V =
evil : Unit -> V
evil = bug ""
scratch/main> add
withV : Unit
withV = match evil () with
x -> ()
unique type SomeType = A
scratch/main> add
unique type R = R SomeType
get x = match x with
R y -> y
unique type R = { someType : SomeType }
Ability handlers
Exhaustive ability handlers are accepted
structural ability Abort where
abort : {Abort} a
result : '{e, Abort} a -> {e} a
result f = handle !f with cases
{ x } -> x
{ abort -> _ } -> bug "aborted"
structural ability Abort where
abort : {Abort} a
unique type T = A | B
result : '{e, Abort} T -> {e} ()
result f = handle !f with cases
{ A } -> ()
{ B } -> ()
{ abort -> _ } -> bug "aborted"
structural ability Abort where
abort : {Abort} a
result : '{e, Abort} V -> {e} V
result f =
impl : Request {Abort} V -> V
impl = cases
{ abort -> _ } -> bug "aborted"
handle !f with impl
structural ability Abort where
abort : {Abort} a
structural ability Stream a where
emit : a -> {Stream a} Unit
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
handleMulti c =
impl xs = cases
{ r } -> (Some r, xs)
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
{ abort -> _ } -> (None, xs)
handle !c with impl []
Non-exhaustive ability handlers are rejected
structural ability Abort where
abort : {Abort} a
abortWithMessage : Text -> {Abort} a
result : '{e, Abort} a -> {e} a
result f = handle !f with cases
{ abort -> _ } -> bug "aborted"
structural ability Abort where
abort : {Abort} a
unique type T = A | B
result : '{e, Abort} T -> {e} ()
result f = handle !f with cases
{ A } -> ()
{ abort -> _ } -> bug "aborted"
unique ability Give a where
give : a -> {Give a} Unit
unique type T = A | B
result : '{e, Give T} r -> {e} r
result f = handle !f with cases
{ x } -> x
{ give A -> resume } -> result resume
structural ability Abort where
abort : {Abort} a
structural ability Stream a where
emit : a -> {Stream a} Unit
handleMulti : '{Stream a, Abort} r -> (Optional r, [a])
handleMulti c =
impl : [a] -> Request {Stream a, Abort} r -> (Optional r, [a])
impl xs = cases
{ r } -> (Some r, xs)
{ emit x -> resume } -> handle !resume with impl (xs :+ x)
handle !c with impl []
Redundant handler cases are rejected
unique ability Give a where
give : a -> {Give a} Unit
unique type T = A | B
result : '{e, Give T} r -> {e} r
result f = handle !f with cases
{ x } -> x
{ give _ -> resume } -> result resume
{ give A -> resume } -> result resume
Exhaustive ability reinterpretations are accepted
structural ability Abort where
abort : {Abort} a
abortWithMessage : Text -> {Abort} a
result : '{e, Abort} a -> {e, Abort} a
result f = handle !f with cases
{ x } -> x
{ abort -> _ } -> abort
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
structural ability Abort a where
abort : {Abort a} r
abortWithMessage : a -> {Abort a} r
result : '{e, Abort V} a -> {e, Abort V} a
result f =
impl : Request {Abort V} r -> {Abort V} r
impl = cases
{ x } -> x
{ abort -> _ } -> abort
handle !f with impl
Non-exhaustive ability reinterpretations are rejected
structural ability Abort where
abort : {Abort} a
abortWithMessage : Text -> {Abort} a
result : '{e, Abort} a -> {e, Abort} a
result f = handle !f with cases
{ x } -> x
{ abortWithMessage msg -> _ } -> abortWithMessage ("aborting: " ++ msg)
Hacky workaround for uninhabited abilities
Although all of the constructors of an ability might be uninhabited, the typechecker requires at least one be specified so that it can determine that the ability should be discharged. So, the default pattern match coverage checking behavior of prohibiting covering any of the cases is problematic. Instead, the pattern match coverage checker will require that at least one constructor be given, even if they are all uninhabited.
The messages here aren't the best, but I don't think uninhabited abilities will come up and get handlers written for them often.
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
handle !f with impl
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
{ give _ -> resume } -> bug "impossible"
handle !f with impl
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
{ give2 _ -> resume } -> bug "impossible"
handle !f with impl
unique ability Give a where
give : a -> {Give a} Unit
give2 : a -> {Give a} Unit
result : '{e, Give V} r -> {e} r
result f =
impl : Request {Give V} r -> {} r
impl = cases
{ x } -> x
{ give _ -> resume } -> bug "impossible"
{ give2 _ -> resume } -> bug "impossible"
handle !f with impl
unique ability GiveA a where
giveA : a -> {GiveA a} Unit
giveA2 : a -> {GiveA a} Unit
unique ability GiveB a where
giveB : a -> {GiveB a} Unit
giveB2 : a -> {GiveB a} Unit
result : '{e, GiveA V, GiveB V} r -> {e} r
result f =
impl : Request {GiveA V, GiveB V} r -> {} r
impl = cases
{ x } -> x
{ giveA _ -> _ } -> bug "impossible"
{ giveA2 _ -> _ } -> bug "impossible"
{ giveB _ -> _ } -> bug "impossible"
{ giveB2 _ -> _ } -> bug "impossible"
handle !f with impl
unique ability GiveA a where
giveA : a -> {GiveA a} Unit
giveA2 : a -> {GiveA a} Unit
unique ability GiveB a where
giveB : a -> {GiveB a} Unit
giveB2 : a -> {GiveB a} Unit
result : '{e, GiveA V, GiveB V} r -> {e} r
result f =
impl : Request {GiveA V, GiveB V} r -> {} r
impl = cases
{ x } -> x
{ giveA2 _ -> _ } -> bug "impossible"
{ giveB _ -> _ } -> bug "impossible"
handle !f with impl