Fixpoint3.Boxing
The purpose of this file is to represent every Boxed value with an Int64.
For all primitive values the Int64 representation is simply the raw bits,
possibly extended to form an Int64.
For BoxedObject some Int64 value is computed to represent it with the
promise that equality is maintained with respect to Order on the BoxedObject.
Consider the following program:
A(x, y) :- B(x), C(y).
We know that A[0] and B[0] should share the same value, and if we project the
representing Int64 from B to A then we should be able to compute the
Boxed value. We therefore unify the two, effectively declaring that the types
are the same. The same is done for A[1] and C[0]. On the other hand unifying
A[0] and A[1] is not secure, as it could mix two unrelated types.
The initialize method computes a unification and transforms all Boxed facts
to Int64 and returns a BoxingType.Boxing.
See BoxingType.flix for data types and an example of how BoxedObjects are treated.
The module operates on Ram.Program, so it uses, Eq(x, y), Meet(x, y), Project(_)
and so on to compute the equality constraints.
Definitions
def boxWith(v: Int64, index: UnifiedTypePos, info: Boxing[r]): Boxed \ r
SourceBoxes v given its type information at typeInfo[index] in info.
Returns v boxed.
def initialize(rc: Region[r], withProv: Bool, program: RamProgram): (Boxing[r], Facts[r]) \ r
SourceReturns a (boxing, facts, idToBoxing) where Boxing is information as described above,
facts are the EDB of program as Int64, with respect to boxing.
def unboxWith(v: Boxed, index: UnifiedTypePos, info: Boxing[r]): Int64 \ r
SourceUnbox v given the type information stored at typeInfo[index] in info.
Returns v unboxed.