Std.Physical

1module Std.Physical
2
3import Model.Config
4import Model.Word32
5import Model.Word64
6import Model.Parameter
7import Std.Word
8
9-- Refined values for safety and ABI boundaries (R4/L32, READ-006). These are
10-- intentionally a small set of roles that are routinely confused at physical
11-- interfaces; this is not a blanket wrapper for every number in the program.
12
13family StdByteCount : Type 0
14constructor StdByteCountOf
15field unrestricted stdByteCountWord : StdU64
16end-family
17
18family StdByteAlignment : Type 0
19constructor StdByteAlignmentOf
20field unrestricted stdByteAlignmentWord : StdU64
21end-family
22
23family StdDeviceAddress : Type 0
24constructor StdDeviceAddressOf
25field unrestricted stdDeviceAddressWord : StdU64
26end-family
27
28family StdGridDimension : Type 0
29constructor StdGridDimensionOf
30field unrestricted stdGridDimensionWord : StdU32
31end-family
32
33family StdRegisterCount : Type 0
34constructor StdRegisterCountOf
35field unrestricted stdRegisterCountWord : StdU32
36end-family
37
38family StdFileDescriptor : Type 0
39constructor StdFileDescriptorOf
40field unrestricted stdFileDescriptorWord : (family StdI32)
41end-family
42
43family StdResourceHandle : Type 0
44constructor StdResourceHandleOf
45field unrestricted stdResourceHandleWord : StdU32
46end-family
47
48family StdTimeoutNanoseconds : Type 0
49constructor StdTimeoutNanosecondsOf
50field unrestricted stdTimeoutNanosecondsWord : StdU64
51end-family
52
53def ByteCount = (family StdByteCount)
54def ByteAlignment = (family StdByteAlignment)
55def DeviceAddress = (family StdDeviceAddress)
56def GridDimension = (family StdGridDimension)
57def RegisterCount = (family StdRegisterCount)
58def FileDescriptor = (family StdFileDescriptor)
59def ResourceHandle = (family StdResourceHandle)
60def TimeoutNanoseconds = (family StdTimeoutNanoseconds)
61
62def stdByteCount =
63  (lambda unrestricted value : StdU64 .
64    (constructor StdByteCount StdByteCountOf value))
65
66def stdByteAlignment =
67  (lambda unrestricted value : StdU64 .
68    (constructor StdByteAlignment StdByteAlignmentOf value))
69
70def stdDeviceAddress =
71  (lambda unrestricted value : StdU64 .
72    (constructor StdDeviceAddress StdDeviceAddressOf value))
73
74def stdGridDimension =
75  (lambda unrestricted value : StdU32 .
76    (constructor StdGridDimension StdGridDimensionOf value))
77
78def stdRegisterCount =
79  (lambda unrestricted value : StdU32 .
80    (constructor StdRegisterCount StdRegisterCountOf value))
81
82def stdFileDescriptor =
83  (lambda unrestricted value : (family StdI32) .
84    (constructor StdFileDescriptor StdFileDescriptorOf value))
85
86def stdResourceHandle =
87  (lambda unrestricted value : StdU32 .
88    (constructor StdResourceHandle StdResourceHandleOf value))
89
90def stdTimeoutNanoseconds =
91  (lambda unrestricted value : StdU64 .
92    (constructor StdTimeoutNanoseconds StdTimeoutNanosecondsOf value))
93
94def stdByteCountValue =
95  (lambda unrestricted value : ByteCount .
96    (eliminate StdByteCount
97      (lambda unrestricted current : ByteCount . StdU64)
98      value
99      (branch StdByteCountOf word . word)))
100
101def stdByteAlignmentValue =
102  (lambda unrestricted value : ByteAlignment .
103    (eliminate StdByteAlignment
104      (lambda unrestricted current : ByteAlignment . StdU64)
105      value
106      (branch StdByteAlignmentOf word . word)))
107
108def stdDeviceAddressValue =
109  (lambda unrestricted value : DeviceAddress .
110    (eliminate StdDeviceAddress
111      (lambda unrestricted current : DeviceAddress . StdU64)
112      value
113      (branch StdDeviceAddressOf word . word)))
114
115def stdGridDimensionValue =
116  (lambda unrestricted value : GridDimension .
117    (eliminate StdGridDimension
118      (lambda unrestricted current : GridDimension . StdU32)
119      value
120      (branch StdGridDimensionOf word . word)))
121
122def stdRegisterCountValue =
123  (lambda unrestricted value : RegisterCount .
124    (eliminate StdRegisterCount
125      (lambda unrestricted current : RegisterCount . StdU32)
126      value
127      (branch StdRegisterCountOf word . word)))
128
129def stdFileDescriptorValue =
130  (lambda unrestricted value : FileDescriptor .
131    (eliminate StdFileDescriptor
132      (lambda unrestricted current : FileDescriptor . (family StdI32))
133      value
134      (branch StdFileDescriptorOf word . word)))
135
136def stdResourceHandleValue =
137  (lambda unrestricted value : ResourceHandle .
138    (eliminate StdResourceHandle
139      (lambda unrestricted current : ResourceHandle . StdU32)
140      value
141      (branch StdResourceHandleOf word . word)))
142
143def stdTimeoutNanosecondsValue =
144  (lambda unrestricted value : TimeoutNanoseconds .
145    (eliminate StdTimeoutNanoseconds
146      (lambda unrestricted current : TimeoutNanoseconds . StdU64)
147      value
148      (branch StdTimeoutNanosecondsOf word . word)))