module Std.Physical

import Model.Config
import Model.Word32
import Model.Word64
import Model.Parameter
import Std.Word

-- Refined values for safety and ABI boundaries (R4/L32, READ-006). These are
-- intentionally a small set of roles that are routinely confused at physical
-- interfaces; this is not a blanket wrapper for every number in the program.

family StdByteCount : Type 0
constructor StdByteCountOf
field unrestricted stdByteCountWord : StdU64
end-family

family StdByteAlignment : Type 0
constructor StdByteAlignmentOf
field unrestricted stdByteAlignmentWord : StdU64
end-family

family StdDeviceAddress : Type 0
constructor StdDeviceAddressOf
field unrestricted stdDeviceAddressWord : StdU64
end-family

family StdGridDimension : Type 0
constructor StdGridDimensionOf
field unrestricted stdGridDimensionWord : StdU32
end-family

family StdRegisterCount : Type 0
constructor StdRegisterCountOf
field unrestricted stdRegisterCountWord : StdU32
end-family

family StdFileDescriptor : Type 0
constructor StdFileDescriptorOf
field unrestricted stdFileDescriptorWord : (family StdI32)
end-family

family StdResourceHandle : Type 0
constructor StdResourceHandleOf
field unrestricted stdResourceHandleWord : StdU32
end-family

family StdTimeoutNanoseconds : Type 0
constructor StdTimeoutNanosecondsOf
field unrestricted stdTimeoutNanosecondsWord : StdU64
end-family

def ByteCount = (family StdByteCount)
def ByteAlignment = (family StdByteAlignment)
def DeviceAddress = (family StdDeviceAddress)
def GridDimension = (family StdGridDimension)
def RegisterCount = (family StdRegisterCount)
def FileDescriptor = (family StdFileDescriptor)
def ResourceHandle = (family StdResourceHandle)
def TimeoutNanoseconds = (family StdTimeoutNanoseconds)

def stdByteCount =
  (lambda unrestricted value : StdU64 .
    (constructor StdByteCount StdByteCountOf value))

def stdByteAlignment =
  (lambda unrestricted value : StdU64 .
    (constructor StdByteAlignment StdByteAlignmentOf value))

def stdDeviceAddress =
  (lambda unrestricted value : StdU64 .
    (constructor StdDeviceAddress StdDeviceAddressOf value))

def stdGridDimension =
  (lambda unrestricted value : StdU32 .
    (constructor StdGridDimension StdGridDimensionOf value))

def stdRegisterCount =
  (lambda unrestricted value : StdU32 .
    (constructor StdRegisterCount StdRegisterCountOf value))

def stdFileDescriptor =
  (lambda unrestricted value : (family StdI32) .
    (constructor StdFileDescriptor StdFileDescriptorOf value))

def stdResourceHandle =
  (lambda unrestricted value : StdU32 .
    (constructor StdResourceHandle StdResourceHandleOf value))

def stdTimeoutNanoseconds =
  (lambda unrestricted value : StdU64 .
    (constructor StdTimeoutNanoseconds StdTimeoutNanosecondsOf value))

def stdByteCountValue =
  (lambda unrestricted value : ByteCount .
    (eliminate StdByteCount
      (lambda unrestricted current : ByteCount . StdU64)
      value
      (branch StdByteCountOf word . word)))

def stdByteAlignmentValue =
  (lambda unrestricted value : ByteAlignment .
    (eliminate StdByteAlignment
      (lambda unrestricted current : ByteAlignment . StdU64)
      value
      (branch StdByteAlignmentOf word . word)))

def stdDeviceAddressValue =
  (lambda unrestricted value : DeviceAddress .
    (eliminate StdDeviceAddress
      (lambda unrestricted current : DeviceAddress . StdU64)
      value
      (branch StdDeviceAddressOf word . word)))

def stdGridDimensionValue =
  (lambda unrestricted value : GridDimension .
    (eliminate StdGridDimension
      (lambda unrestricted current : GridDimension . StdU32)
      value
      (branch StdGridDimensionOf word . word)))

def stdRegisterCountValue =
  (lambda unrestricted value : RegisterCount .
    (eliminate StdRegisterCount
      (lambda unrestricted current : RegisterCount . StdU32)
      value
      (branch StdRegisterCountOf word . word)))

def stdFileDescriptorValue =
  (lambda unrestricted value : FileDescriptor .
    (eliminate StdFileDescriptor
      (lambda unrestricted current : FileDescriptor . (family StdI32))
      value
      (branch StdFileDescriptorOf word . word)))

def stdResourceHandleValue =
  (lambda unrestricted value : ResourceHandle .
    (eliminate StdResourceHandle
      (lambda unrestricted current : ResourceHandle . StdU32)
      value
      (branch StdResourceHandleOf word . word)))

def stdTimeoutNanosecondsValue =
  (lambda unrestricted value : TimeoutNanoseconds .
    (eliminate StdTimeoutNanoseconds
      (lambda unrestricted current : TimeoutNanoseconds . StdU64)
      value
      (branch StdTimeoutNanosecondsOf word . word)))