Pattern Matching: anomaly detection

Melwyn Saldanha requested to merge melwyn95/pm/case-analysis into dev

type:changed

Implemented the alorithms from "Warnings for pattern matching" to detect anomalies in pattern matching.

Flow:

  1. After patterns are type-checked we get typed patterns
  2. The typed patterns are flattened into simple_pattern (flat representation of patterns)
  3. Anomalies are detected using algorithm_Urec & algorithm_I
  4. In case of missing cases, we get the missing simple_pattern's, then we convert the simple_patterns to original patterns (LIGO patterns) using the type information
  5. 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

Merge request reports