Fixpoint3.Boxing

Definitions

def boxWith(v: Int64, index: UnifiedTypePos, info: Boxing[r]): Boxed \ r Source

Boxes 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 Source

Returns 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 Source

Unbox v given the type information stored at typeInfo[index] in info. Returns v unboxed.