Fixpoint3.BoxingType

The purpose of this file is to record the transformation from Boxed values to Int64.

The interpreter works with tuples as Vectors of Int64. We therefore map all objects to an Int64. For all primitive data types, this is straightforward as they all fit in an Int64. For objects, we store them in a map from the Boxed object to the Int64, which the interpreter can work with.

Since data can flow between relations in the interpreter, we need to somehow keep track of where the different Int64's came from. Consider the following program

B(1 :: Nil, 42)
A(x, y) :- B(x, y)

The term 1 :: Nil would map to e.g. 0, resulting in the program

B(0, 42)
A(x, y) :- B(x, y)

At some point, 0 must be transformed back to 1 :: Nil. For this program, Boxing would be

(
   Vector#{MutList#{1 :: Nil}, MutList#{}},
   Vector#{BPlusTree#{1 :: Nil -> 0}, BPlusTree#{}},
   Vector#{Array#{Types.Object, Types.Int32}},
   Vector#{Lock1, Lock2},
)

We then store the fact that the type-information about A[0] and B[0] are stored at UnifiedTypePos 0 and A[1] and B[1] are stored at position 1. We only need to keep the MutList and BPlusTree for objects, as transforming the simple types requires less information.