Parametric type variables and Datatype parameters

[philzook58]

I'm using the python API for building a proof assistant. I can deal with notions of genericity via using python functions def List(T): ... that build new sorts for particular instantiations of Lists or tuples say, but it would be nice to have the notion of List<A> available. AFAIK this is in the syntax of smtlib but not available through the bindings? Maybe I could use parse_smtlib2_string to get more functionality here than what is available though the api? I'm not sure if the new smtlib2.7 has bearing on this or not.

There is what I understand to be tentative support for DeclareTypeVar which would be preferable to using the meta python when I want to translate some Isabelle or HOL light axiomatization as they use at least parametric types liberally.

The current behavior of type variables seems to be doing something like existential types when they go into the definition of a datatype.

from z3 import *
T = DeclareTypeVar("T")
List = Datatype("List")
List.declare("nil")
List.declare("cons", ("car", T), ("cdr", List))
List = List.create()
ilist = List.cons(IntVal(3), List.nil)
rlist = List.cons(RealVal(3), List.nil)
assert ilist.sort() == rlist.sort() 
assert List.car(ilist).sort() == List.car(rlist).sort() # same sort = T. Odd. But reasonable maybe.

I'm not exactly clear on what I may be missing or suggesting, so I thought maybe initiating a discussion could be helpful. Thanks.

[philzook58]

I'm also unclear what happens when Arrays have polymorphic arguments or results.

Here is an attempt to write down and apply a recursor for the Nats.

from z3 import *
Nat = Datatype("Nat")
Nat.declare("Z")
Nat.declare("S", ("pred", Nat))
Nat = Nat.create()

a = DeclareTypeVar("a")

x = Const("x", Nat)
base = Const("base", a)
f = Const("f", ArraySort(a, a))
rec = Function("rec", Nat, a, ArraySort(a, a), a)

rec(x, base, f) == If(x == Nat.Z, base, f[rec(Nat.pred(x), base, f)]) # This is fine

p = Array("p", Nat, Nat)
rec(Nat.Z, Nat.Z, p) # This is a Sort mismatch error