[CN-Exec] Incorrect Redundant patterns error for nested patterns

[ZippeyKeys12]

To reproduce, call cn instrument on the following code.

/*@
datatype Example {
  Leaf {},
  Node { Example x }
}

function (datatype Example) func(datatype Example ex) {
  match ex {
    Node { x: Node { x: y } } => {
      y
    }
    _  => { ex }
  }
}
@*/

int main() { return 0; }

to get:

cn: internal error, uncaught exception:
    Failure("Redundant patterns")

Full error

cn: internal error, uncaught exception:
    Failure("Redundant patterns")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__Cn_internal_to_ail.cn_to_ail_expr_aux_internal.translate.build_case in file "backend/cn/lib/cn_internal_to_ail.ml", line 1477, characters 19-73
    Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
    Called from Cn__Cn_internal_to_ail.cn_to_ail_expr_aux_internal.translate in file "backend/cn/lib/cn_internal_to_ail.ml", line 1506, characters 36-70
    Called from Cn__Cn_internal_to_ail.cn_to_ail_expr_aux_internal.translate.build_case in file "backend/cn/lib/cn_internal_to_ail.ml", line 1477, characters 19-73
    Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
    Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
    Called from Cn__Cn_internal_to_ail.cn_to_ail_expr_aux_internal.translate in file "backend/cn/lib/cn_internal_to_ail.ml", line 1506, characters 36-70
    Called from Cn__Cn_internal_to_ail.cn_to_ail_expr_internal_with_pred_name in file "backend/cn/lib/cn_internal_to_ail.ml" (inlined), line 1598, characters 2-70
    Called from Cn__Cn_internal_to_ail.cn_to_ail_function_internal in file "backend/cn/lib/cn_internal_to_ail.ml", line 2948, characters 8-86
    Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
    Called from Cn__Executable_spec_internal.generate_c_functions_internal in file "backend/cn/lib/executable_spec_internal.ml", line 376, characters 4-183
    Called from Cn__Executable_spec.main.(fun) in file "backend/cn/lib/executable_spec.ml", line 233, characters 4-63
    Called from Dune__exe__Main.generate_executable_specs.(fun) in file "backend/cn/bin/main.ml", line 405, characters 10-275
    Called from Cerb_colour.without_colour in file "util/cerb_colour.ml", line 40, characters 10-13
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 157, characters 6-442
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 176, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44

It can be worked around by not using nested patterns and using nested matches instead as shown below:

/*@
datatype Example {
  Leaf {},
  Node { Example x }
}

function (datatype Example) func(datatype Example ex) {
  match ex {
    Node { x: tmp } => {
      match tmp {
        Node { x: y } => { y }
        Leaf {} => { ex }
      }
    }
    Leaf {} => { ex }
  }
}
@*/

int main() { return 0; }