kdrag.datatype.datatype_match_

kdrag.datatype.datatype_match_(x, *cases, default=None)

Pattern matching for datatypes.

>>> import kdrag.theories.nat as nat
>>> x = smt.Const("x", nat.Nat)
>>> x.match_((nat.S(x), nat.S(x)), (nat.one, nat.one), default=x)
If(is(S, x),
   S(pred(x)),
   If(And(is(S, x), is(Z, pred(x))), S(Z), x))

>>> import kdrag.theories.list as list_
>>> IntList = list_.List(smt.IntSort())
>>> l = smt.Const("l", IntList)
>>> x,y,z = smt.Ints("x y z")
>>> l.match_((IntList.Nil, 0), (IntList.Cons(x, l), 1 + x))
If(is(Nil, l),
   0,
   If(is(Cons, l), 1 + head(l), unreachable!...))