Pattern Matching: anomaly detection
type:changed
Implemented the alorithms from "Warnings for pattern matching" to detect anomalies in pattern matching.
Flow:
- After patterns are type-checked we get typed patterns
- The typed patterns are flattened into
simple_pattern
(flat representation of patterns) - Anomalies are detected using
algorithm_Urec
&algorithm_I
- In case of missing cases, we get the missing
simple_pattern
's, then we convert thesimple_patterns
to original patterns (LIGO patterns) using the type information - In case of redundant case, we get the redundant pattern, we show an error message with location of the redundant pattern
Changelog details:
Improve pattern matching anomaly (missing case / redundant case) error messages.
For missing cases:
type p = Four | Five | Six
type t = One of { a : int ; b : p } | Two | Three
let s (x : t) =
match x with
One { a ; b = Six } -> ()
| Two -> ()
| Three -> ()
Error:
File "../../test/contracts/negative//pattern_matching_anomalies/missing_cases/c_r_c.mligo", line 5, character 2 to line 8, character 29:
4 | let s (x : t) =
5 | match x with
6 | One { a ; b = Six } -> ()
7 | | Two -> ()
8 | | Three -> ()
Error : this pattern-matching is not exhaustive.
Here are examples of cases that are not matched:
- One({ a = _ ; b = Five })
- One({ a = _ ; b = Four })
For redundant case:
type t = One of int | Two of nat | Three
let s (x : t) =
match x with
One a -> ()
| Two c -> ()
| Three -> ()
| _ -> ()
Error:
File "../../test/contracts/negative//pattern_matching_anomalies/redundant_case/c1_c2_c3_w.mligo", line 8, characters 4-5:
7 | | Three -> ()
8 | | _ -> ()
Error : this match case is unused
Edited by Melwyn Saldanha