Source/Systems

Coppelius.Build.DeviceImages

systems/coppelius/src/Coppelius/Build/DeviceImages.alpha

726 lines107 declarations39.5 KiBSHA-256 aca105a01057

def · lines 289–305

coppeliusDeviceImage

Full file
An image: its typed program, and the program's SM86 encoding, which places it (Coppelius.Build.Graph names launches by that placement); the backend realizes the region in the target's machine code. Its program's halves are in the plan's format (Coppelius.Learner).
289def coppeliusDeviceImage =
290  (lambda unrestricted identity : Bytes .
291    (lambda unrestricted program : (family SM86Program) .
292      (lambda unrestricted registers : Nat .
293        (lambda unrestricted blockX : Nat .
294          (lambda unrestricted sharedBytes : Nat .
295            (let unrestricted halves = (sm86ProgramWithHalfFormat coppeliusHalfFormat program) in
296            (let unrestricted guarded = (coppeliusGuardLateReadsIfRequired halves) in
297            (constructor
298              CoppeliusDeviceImage
299              CoppeliusDeviceImageValue
300              identity
301              guarded
302              (coppeliusProgramImage guarded)
303              registers
304              blockX
305              sharedBytes))))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.