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?
Structs can refer to themselves both directly and indirectly. Take the following struct, implementing a simple linked list of i32s:
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":
Regardless, this is still a very tough topic for WhyR generation. What about more complex recursion cases, for instance?