declaring algebraic data type of another algebraic data type?

Question

I'm wondering if it's possible to create a algebraic data type that depends on another algebraic data type in Z3Py.

Example, say I defined my own Bool data type and I want to define a List of Bool myself:

from z3 import *
Bool = Datatype('Bool')
Bool.declare('TRUE')
Bool.declare('FALSE')
Bool = Bool.create()
TRUE = Bool.TRUE
FALSE = Bool.FALSE

this works fine, then:

BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
BoolList = BoolList.create()

This fails with the message:

>>> BoolList.declare('bCONS', ('hd', Bool()), ('tail', BoolList))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
AttributeError: DatatypeSortRef instance has no __call__ method

the reason is the usage of Bool() as a reference to an earlier defined data type. Using the Z3 boolean sort instead works like a charm:

BoolList = Datatype('BoolList')
BoolList.declare('bNIL')
BoolList.declare('bCONS', ('hd', BoolSort()), ('tail', BoolList))

Is the definition of an algebraic data type that depends on another algebraic data types impossible or do I need to pass s.th. else than Bool() ?

Thanks in advance! Carsten

Answer 1

Well, it turns out I used brackets where I shouldn't - the reference to the custom data type "Bool" needs no call:

BoolList.declare('bCONS', ('hd', Bool), ('tail', BoolList))

works just fine :)