Module ElimPatternMatch

module ElimPatternMatch: sig .. end

Eliminate pattern-matching in Terms

Eliminate terms match t with A x -> a | B -> b | C y z -> c into if is-A t then a[x := select-A-0 t] else if is-B t then b else c[y := select-C-0 t, z := select-C-1 t]

which is a decision tree understandable by CVC4

type term = Nunchaku_core.TermInner.Default.t

type mode =

`\|`	`Elim_data_match`
`\|`	`Elim_codata_match`
`\|`	`Elim_both`

Mode of operations: which matches should be removed?

val name : string

val tr_problem : ?mode:mode ->
       (term, term) Nunchaku_core.Problem.t ->
       (term, term) Nunchaku_core.Problem.t

val pipe : mode:mode ->
       print:bool ->
       check:bool ->
       ((term, term) Nunchaku_core.Problem.t,
        (term, term) Nunchaku_core.Problem.t, 'c,
        'c)
       Nunchaku_core.Transform.t

Pipeline component. Reverse direction is identity.