Handling of Recursive Structs

[iconmaster5326]

Structs can refer to themselves both directly and indirectly. Take the following struct, implementing a simple linked list of i32s:

%int_list = type {i32, %int_list*}

How does this generate to Why3? Theories cannot be forward-declared, but the definition of the type %int_list depends on the definition of the type %int_list*, and vice versa. How can we resolve this?

Here is one solution, using the already-existing WhyR types "pointer" and "i32":

type pointer_struct_int_list_box

function box_pointer_struct_int_list (pointer 'a) : pointer_struct_int_list_box
function unbox_pointer_struct_int_list pointer_struct_int_list_box :(pointer 'a)

type struct_int_list = {
    x : i32;
    y : pointer_gen;
}

function make_struct_int_list (i:i32) (p:(pointer struct_int_list)) :struct_int_list = {x = i; y = (box_pointer_struct_int_list p);}
axiom make_struct_int_list: forall i. forall p : (pointer struct_int_list). (unbox_pointer_struct_int_list (make_struct_int_list i p).y) = p

Regardless, this is still a very tough topic for WhyR generation. What about more complex recursion cases, for instance?