---
# System prepended metadata

title: pattern matching
tags: [violet]

---

---
tags: violet
---
# pattern matching

- [x] simple pattern matching 的 eval
- [x] simple pattern matching 的 type check
- [ ] simple pattern 的 cover check

simple pattern 在我們這裡的解釋是只有一個正規的 constructor head 跟一串 variables，舉例來說
```
data Nat
| zero
| suc Nat

match n
| zero => ...
| suc n => ...
```

這裡的 pattern 都是 simple pattern，而要是有

```
match n
| zero => ...
| _ => ...
```

wildcard 是任意 match，且捨棄內容，這就不是 simple pattern

## complex pattern 語法糖

complex pattern 就有各種可能性，而我們會需要一個特殊的函數，簽名是 `ComplexPattern -> SimplePattern`

- [ ] wildcard pattern, e.g. `_`
- [ ] nested pattern, e.g. `suc (suc n)`
- [ ] or pattern, e.g. `| one | two => ...` （只需要複製 rhs 就好了）
- [ ] let single pattern 語法，這個情況是當 constructor 是唯一的的時候，那用 let binding 直接解開是合理的
- [ ] if let 語法，等於 `match e | C => ... | _ => ...`

### References

1. dependent pattern matching elimination: https://static.googleusercontent.com/media/research.google.com/zh-TW//pubs/archive/99.pdf
2. overlapping pattern: https://jesper.sikanda.be/files/overlapping-and-order-independent-patterns.pdf

