83 type serialBufferType =
84 | Eight of BitVector.byte
85 | Nine of BitVector.bit * BitVector.byte
87 (** val serialBufferType_rect_Type4 :
88 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
89 serialBufferType -> 'a1 **)
90 let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
91 | Eight x_8 -> h_Eight x_8
92 | Nine (x_10, x_9) -> h_Nine x_10 x_9
94 (** val serialBufferType_rect_Type5 :
95 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
96 serialBufferType -> 'a1 **)
97 let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
98 | Eight x_14 -> h_Eight x_14
99 | Nine (x_16, x_15) -> h_Nine x_16 x_15
101 (** val serialBufferType_rect_Type3 :
102 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
103 serialBufferType -> 'a1 **)
104 let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
105 | Eight x_20 -> h_Eight x_20
106 | Nine (x_22, x_21) -> h_Nine x_22 x_21
108 (** val serialBufferType_rect_Type2 :
109 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
110 serialBufferType -> 'a1 **)
111 let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
112 | Eight x_26 -> h_Eight x_26
113 | Nine (x_28, x_27) -> h_Nine x_28 x_27
115 (** val serialBufferType_rect_Type1 :
116 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
117 serialBufferType -> 'a1 **)
118 let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
119 | Eight x_32 -> h_Eight x_32
120 | Nine (x_34, x_33) -> h_Nine x_34 x_33
122 (** val serialBufferType_rect_Type0 :
123 (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
124 serialBufferType -> 'a1 **)
125 let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
126 | Eight x_38 -> h_Eight x_38
127 | Nine (x_40, x_39) -> h_Nine x_40 x_39
129 (** val serialBufferType_inv_rect_Type4 :
130 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
131 BitVector.byte -> __ -> 'a1) -> 'a1 **)
132 let serialBufferType_inv_rect_Type4 hterm h1 h2 =
133 let hcut = serialBufferType_rect_Type4 h1 h2 hterm in hcut __
135 (** val serialBufferType_inv_rect_Type3 :
136 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
137 BitVector.byte -> __ -> 'a1) -> 'a1 **)
138 let serialBufferType_inv_rect_Type3 hterm h1 h2 =
139 let hcut = serialBufferType_rect_Type3 h1 h2 hterm in hcut __
141 (** val serialBufferType_inv_rect_Type2 :
142 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
143 BitVector.byte -> __ -> 'a1) -> 'a1 **)
144 let serialBufferType_inv_rect_Type2 hterm h1 h2 =
145 let hcut = serialBufferType_rect_Type2 h1 h2 hterm in hcut __
147 (** val serialBufferType_inv_rect_Type1 :
148 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
149 BitVector.byte -> __ -> 'a1) -> 'a1 **)
150 let serialBufferType_inv_rect_Type1 hterm h1 h2 =
151 let hcut = serialBufferType_rect_Type1 h1 h2 hterm in hcut __
153 (** val serialBufferType_inv_rect_Type0 :
154 serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
155 BitVector.byte -> __ -> 'a1) -> 'a1 **)
156 let serialBufferType_inv_rect_Type0 hterm h1 h2 =
157 let hcut = serialBufferType_rect_Type0 h1 h2 hterm in hcut __
159 (** val serialBufferType_discr :
160 serialBufferType -> serialBufferType -> __ **)
161 let serialBufferType_discr x y =
162 Logic.eq_rect_Type2 x
164 | Eight a0 -> Obj.magic (fun _ dH -> dH __)
165 | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
167 (** val serialBufferType_jmdiscr :
168 serialBufferType -> serialBufferType -> __ **)
169 let serialBufferType_jmdiscr x y =
170 Logic.eq_rect_Type2 x
172 | Eight a0 -> Obj.magic (fun _ dH -> dH __)
173 | Nine (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
176 | P1 of BitVector.byte
177 | P3 of BitVector.byte
178 | SerialBuffer of serialBufferType
180 (** val lineType_rect_Type4 :
181 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
182 -> 'a1) -> lineType -> 'a1 **)
183 let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
184 | P1 x_87 -> h_P1 x_87
185 | P3 x_88 -> h_P3 x_88
186 | SerialBuffer x_89 -> h_SerialBuffer x_89
188 (** val lineType_rect_Type5 :
189 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
190 -> 'a1) -> lineType -> 'a1 **)
191 let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
192 | P1 x_94 -> h_P1 x_94
193 | P3 x_95 -> h_P3 x_95
194 | SerialBuffer x_96 -> h_SerialBuffer x_96
196 (** val lineType_rect_Type3 :
197 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
198 -> 'a1) -> lineType -> 'a1 **)
199 let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
200 | P1 x_101 -> h_P1 x_101
201 | P3 x_102 -> h_P3 x_102
202 | SerialBuffer x_103 -> h_SerialBuffer x_103
204 (** val lineType_rect_Type2 :
205 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
206 -> 'a1) -> lineType -> 'a1 **)
207 let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
208 | P1 x_108 -> h_P1 x_108
209 | P3 x_109 -> h_P3 x_109
210 | SerialBuffer x_110 -> h_SerialBuffer x_110
212 (** val lineType_rect_Type1 :
213 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
214 -> 'a1) -> lineType -> 'a1 **)
215 let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
216 | P1 x_115 -> h_P1 x_115
217 | P3 x_116 -> h_P3 x_116
218 | SerialBuffer x_117 -> h_SerialBuffer x_117
220 (** val lineType_rect_Type0 :
221 (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType
222 -> 'a1) -> lineType -> 'a1 **)
223 let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
224 | P1 x_122 -> h_P1 x_122
225 | P3 x_123 -> h_P3 x_123
226 | SerialBuffer x_124 -> h_SerialBuffer x_124
228 (** val lineType_inv_rect_Type4 :
229 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
230 'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
231 let lineType_inv_rect_Type4 hterm h1 h2 h3 =
232 let hcut = lineType_rect_Type4 h1 h2 h3 hterm in hcut __
234 (** val lineType_inv_rect_Type3 :
235 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
236 'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
237 let lineType_inv_rect_Type3 hterm h1 h2 h3 =
238 let hcut = lineType_rect_Type3 h1 h2 h3 hterm in hcut __
240 (** val lineType_inv_rect_Type2 :
241 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
242 'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
243 let lineType_inv_rect_Type2 hterm h1 h2 h3 =
244 let hcut = lineType_rect_Type2 h1 h2 h3 hterm in hcut __
246 (** val lineType_inv_rect_Type1 :
247 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
248 'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
249 let lineType_inv_rect_Type1 hterm h1 h2 h3 =
250 let hcut = lineType_rect_Type1 h1 h2 h3 hterm in hcut __
252 (** val lineType_inv_rect_Type0 :
253 lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ ->
254 'a1) -> (serialBufferType -> __ -> 'a1) -> 'a1 **)
255 let lineType_inv_rect_Type0 hterm h1 h2 h3 =
256 let hcut = lineType_rect_Type0 h1 h2 h3 hterm in hcut __
258 (** val lineType_discr : lineType -> lineType -> __ **)
259 let lineType_discr x y =
260 Logic.eq_rect_Type2 x
262 | P1 a0 -> Obj.magic (fun _ dH -> dH __)
263 | P3 a0 -> Obj.magic (fun _ dH -> dH __)
264 | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
266 (** val lineType_jmdiscr : lineType -> lineType -> __ **)
267 let lineType_jmdiscr x y =
268 Logic.eq_rect_Type2 x
270 | P1 a0 -> Obj.magic (fun _ dH -> dH __)
271 | P3 a0 -> Obj.magic (fun _ dH -> dH __)
272 | SerialBuffer a0 -> Obj.magic (fun _ dH -> dH __)) y
295 (** val sFR8051_rect_Type4 :
296 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
297 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
298 let rec sFR8051_rect_Type4 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
300 | SFR_DPL -> h_SFR_DPL
301 | SFR_DPH -> h_SFR_DPH
302 | SFR_PCON -> h_SFR_PCON
303 | SFR_TCON -> h_SFR_TCON
304 | SFR_TMOD -> h_SFR_TMOD
305 | SFR_TL0 -> h_SFR_TL0
306 | SFR_TL1 -> h_SFR_TL1
307 | SFR_TH0 -> h_SFR_TH0
308 | SFR_TH1 -> h_SFR_TH1
310 | SFR_SCON -> h_SFR_SCON
311 | SFR_SBUF -> h_SFR_SBUF
315 | SFR_PSW -> h_SFR_PSW
316 | SFR_ACC_A -> h_SFR_ACC_A
317 | SFR_ACC_B -> h_SFR_ACC_B
319 (** val sFR8051_rect_Type5 :
320 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
321 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
322 let rec sFR8051_rect_Type5 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
324 | SFR_DPL -> h_SFR_DPL
325 | SFR_DPH -> h_SFR_DPH
326 | SFR_PCON -> h_SFR_PCON
327 | SFR_TCON -> h_SFR_TCON
328 | SFR_TMOD -> h_SFR_TMOD
329 | SFR_TL0 -> h_SFR_TL0
330 | SFR_TL1 -> h_SFR_TL1
331 | SFR_TH0 -> h_SFR_TH0
332 | SFR_TH1 -> h_SFR_TH1
334 | SFR_SCON -> h_SFR_SCON
335 | SFR_SBUF -> h_SFR_SBUF
339 | SFR_PSW -> h_SFR_PSW
340 | SFR_ACC_A -> h_SFR_ACC_A
341 | SFR_ACC_B -> h_SFR_ACC_B
343 (** val sFR8051_rect_Type3 :
344 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
345 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
346 let rec sFR8051_rect_Type3 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
348 | SFR_DPL -> h_SFR_DPL
349 | SFR_DPH -> h_SFR_DPH
350 | SFR_PCON -> h_SFR_PCON
351 | SFR_TCON -> h_SFR_TCON
352 | SFR_TMOD -> h_SFR_TMOD
353 | SFR_TL0 -> h_SFR_TL0
354 | SFR_TL1 -> h_SFR_TL1
355 | SFR_TH0 -> h_SFR_TH0
356 | SFR_TH1 -> h_SFR_TH1
358 | SFR_SCON -> h_SFR_SCON
359 | SFR_SBUF -> h_SFR_SBUF
363 | SFR_PSW -> h_SFR_PSW
364 | SFR_ACC_A -> h_SFR_ACC_A
365 | SFR_ACC_B -> h_SFR_ACC_B
367 (** val sFR8051_rect_Type2 :
368 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
369 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
370 let rec sFR8051_rect_Type2 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
372 | SFR_DPL -> h_SFR_DPL
373 | SFR_DPH -> h_SFR_DPH
374 | SFR_PCON -> h_SFR_PCON
375 | SFR_TCON -> h_SFR_TCON
376 | SFR_TMOD -> h_SFR_TMOD
377 | SFR_TL0 -> h_SFR_TL0
378 | SFR_TL1 -> h_SFR_TL1
379 | SFR_TH0 -> h_SFR_TH0
380 | SFR_TH1 -> h_SFR_TH1
382 | SFR_SCON -> h_SFR_SCON
383 | SFR_SBUF -> h_SFR_SBUF
387 | SFR_PSW -> h_SFR_PSW
388 | SFR_ACC_A -> h_SFR_ACC_A
389 | SFR_ACC_B -> h_SFR_ACC_B
391 (** val sFR8051_rect_Type1 :
392 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
393 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
394 let rec sFR8051_rect_Type1 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
396 | SFR_DPL -> h_SFR_DPL
397 | SFR_DPH -> h_SFR_DPH
398 | SFR_PCON -> h_SFR_PCON
399 | SFR_TCON -> h_SFR_TCON
400 | SFR_TMOD -> h_SFR_TMOD
401 | SFR_TL0 -> h_SFR_TL0
402 | SFR_TL1 -> h_SFR_TL1
403 | SFR_TH0 -> h_SFR_TH0
404 | SFR_TH1 -> h_SFR_TH1
406 | SFR_SCON -> h_SFR_SCON
407 | SFR_SBUF -> h_SFR_SBUF
411 | SFR_PSW -> h_SFR_PSW
412 | SFR_ACC_A -> h_SFR_ACC_A
413 | SFR_ACC_B -> h_SFR_ACC_B
415 (** val sFR8051_rect_Type0 :
416 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
417 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1 **)
418 let rec sFR8051_rect_Type0 h_SFR_SP h_SFR_DPL h_SFR_DPH h_SFR_PCON h_SFR_TCON h_SFR_TMOD h_SFR_TL0 h_SFR_TL1 h_SFR_TH0 h_SFR_TH1 h_SFR_P1 h_SFR_SCON h_SFR_SBUF h_SFR_IE h_SFR_P3 h_SFR_IP h_SFR_PSW h_SFR_ACC_A h_SFR_ACC_B = function
420 | SFR_DPL -> h_SFR_DPL
421 | SFR_DPH -> h_SFR_DPH
422 | SFR_PCON -> h_SFR_PCON
423 | SFR_TCON -> h_SFR_TCON
424 | SFR_TMOD -> h_SFR_TMOD
425 | SFR_TL0 -> h_SFR_TL0
426 | SFR_TL1 -> h_SFR_TL1
427 | SFR_TH0 -> h_SFR_TH0
428 | SFR_TH1 -> h_SFR_TH1
430 | SFR_SCON -> h_SFR_SCON
431 | SFR_SBUF -> h_SFR_SBUF
435 | SFR_PSW -> h_SFR_PSW
436 | SFR_ACC_A -> h_SFR_ACC_A
437 | SFR_ACC_B -> h_SFR_ACC_B
439 (** val sFR8051_inv_rect_Type4 :
440 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
441 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
442 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
443 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
445 let sFR8051_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
447 sFR8051_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
452 (** val sFR8051_inv_rect_Type3 :
453 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
454 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
455 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
456 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
458 let sFR8051_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
460 sFR8051_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
465 (** val sFR8051_inv_rect_Type2 :
466 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
467 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
468 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
469 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
471 let sFR8051_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
473 sFR8051_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
478 (** val sFR8051_inv_rect_Type1 :
479 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
480 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
481 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
482 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
484 let sFR8051_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
486 sFR8051_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
491 (** val sFR8051_inv_rect_Type0 :
492 sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
493 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
494 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
495 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
497 let sFR8051_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 =
499 sFR8051_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16
504 (** val sFR8051_discr : sFR8051 -> sFR8051 -> __ **)
505 let sFR8051_discr x y =
506 Logic.eq_rect_Type2 x
508 | SFR_SP -> Obj.magic (fun _ dH -> dH)
509 | SFR_DPL -> Obj.magic (fun _ dH -> dH)
510 | SFR_DPH -> Obj.magic (fun _ dH -> dH)
511 | SFR_PCON -> Obj.magic (fun _ dH -> dH)
512 | SFR_TCON -> Obj.magic (fun _ dH -> dH)
513 | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
514 | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
515 | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
516 | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
517 | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
518 | SFR_P1 -> Obj.magic (fun _ dH -> dH)
519 | SFR_SCON -> Obj.magic (fun _ dH -> dH)
520 | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
521 | SFR_IE -> Obj.magic (fun _ dH -> dH)
522 | SFR_P3 -> Obj.magic (fun _ dH -> dH)
523 | SFR_IP -> Obj.magic (fun _ dH -> dH)
524 | SFR_PSW -> Obj.magic (fun _ dH -> dH)
525 | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
526 | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
528 (** val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __ **)
529 let sFR8051_jmdiscr x y =
530 Logic.eq_rect_Type2 x
532 | SFR_SP -> Obj.magic (fun _ dH -> dH)
533 | SFR_DPL -> Obj.magic (fun _ dH -> dH)
534 | SFR_DPH -> Obj.magic (fun _ dH -> dH)
535 | SFR_PCON -> Obj.magic (fun _ dH -> dH)
536 | SFR_TCON -> Obj.magic (fun _ dH -> dH)
537 | SFR_TMOD -> Obj.magic (fun _ dH -> dH)
538 | SFR_TL0 -> Obj.magic (fun _ dH -> dH)
539 | SFR_TL1 -> Obj.magic (fun _ dH -> dH)
540 | SFR_TH0 -> Obj.magic (fun _ dH -> dH)
541 | SFR_TH1 -> Obj.magic (fun _ dH -> dH)
542 | SFR_P1 -> Obj.magic (fun _ dH -> dH)
543 | SFR_SCON -> Obj.magic (fun _ dH -> dH)
544 | SFR_SBUF -> Obj.magic (fun _ dH -> dH)
545 | SFR_IE -> Obj.magic (fun _ dH -> dH)
546 | SFR_P3 -> Obj.magic (fun _ dH -> dH)
547 | SFR_IP -> Obj.magic (fun _ dH -> dH)
548 | SFR_PSW -> Obj.magic (fun _ dH -> dH)
549 | SFR_ACC_A -> Obj.magic (fun _ dH -> dH)
550 | SFR_ACC_B -> Obj.magic (fun _ dH -> dH)) y
552 (** val sfr_8051_index : sFR8051 -> Nat.nat **)
553 let sfr_8051_index = function
555 | SFR_DPL -> Nat.S Nat.O
556 | SFR_DPH -> Nat.S (Nat.S Nat.O)
557 | SFR_PCON -> Nat.S (Nat.S (Nat.S Nat.O))
558 | SFR_TCON -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
559 | SFR_TMOD -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
560 | SFR_TL0 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
561 | SFR_TL1 -> Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
563 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
565 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
567 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
570 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
573 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
574 (Nat.S Nat.O)))))))))))
576 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
577 (Nat.S (Nat.S Nat.O))))))))))))
579 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
580 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))
582 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
583 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))
585 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
586 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))
588 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
589 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
591 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
592 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))
601 (** val sFR8052_rect_Type4 :
602 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
603 let rec sFR8052_rect_Type4 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
604 | SFR_T2CON -> h_SFR_T2CON
605 | SFR_RCAP2L -> h_SFR_RCAP2L
606 | SFR_RCAP2H -> h_SFR_RCAP2H
607 | SFR_TL2 -> h_SFR_TL2
608 | SFR_TH2 -> h_SFR_TH2
610 (** val sFR8052_rect_Type5 :
611 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
612 let rec sFR8052_rect_Type5 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
613 | SFR_T2CON -> h_SFR_T2CON
614 | SFR_RCAP2L -> h_SFR_RCAP2L
615 | SFR_RCAP2H -> h_SFR_RCAP2H
616 | SFR_TL2 -> h_SFR_TL2
617 | SFR_TH2 -> h_SFR_TH2
619 (** val sFR8052_rect_Type3 :
620 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
621 let rec sFR8052_rect_Type3 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
622 | SFR_T2CON -> h_SFR_T2CON
623 | SFR_RCAP2L -> h_SFR_RCAP2L
624 | SFR_RCAP2H -> h_SFR_RCAP2H
625 | SFR_TL2 -> h_SFR_TL2
626 | SFR_TH2 -> h_SFR_TH2
628 (** val sFR8052_rect_Type2 :
629 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
630 let rec sFR8052_rect_Type2 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
631 | SFR_T2CON -> h_SFR_T2CON
632 | SFR_RCAP2L -> h_SFR_RCAP2L
633 | SFR_RCAP2H -> h_SFR_RCAP2H
634 | SFR_TL2 -> h_SFR_TL2
635 | SFR_TH2 -> h_SFR_TH2
637 (** val sFR8052_rect_Type1 :
638 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
639 let rec sFR8052_rect_Type1 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
640 | SFR_T2CON -> h_SFR_T2CON
641 | SFR_RCAP2L -> h_SFR_RCAP2L
642 | SFR_RCAP2H -> h_SFR_RCAP2H
643 | SFR_TL2 -> h_SFR_TL2
644 | SFR_TH2 -> h_SFR_TH2
646 (** val sFR8052_rect_Type0 :
647 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1 **)
648 let rec sFR8052_rect_Type0 h_SFR_T2CON h_SFR_RCAP2L h_SFR_RCAP2H h_SFR_TL2 h_SFR_TH2 = function
649 | SFR_T2CON -> h_SFR_T2CON
650 | SFR_RCAP2L -> h_SFR_RCAP2L
651 | SFR_RCAP2H -> h_SFR_RCAP2H
652 | SFR_TL2 -> h_SFR_TL2
653 | SFR_TH2 -> h_SFR_TH2
655 (** val sFR8052_inv_rect_Type4 :
656 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
657 (__ -> 'a1) -> 'a1 **)
658 let sFR8052_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
659 let hcut = sFR8052_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
661 (** val sFR8052_inv_rect_Type3 :
662 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
663 (__ -> 'a1) -> 'a1 **)
664 let sFR8052_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
665 let hcut = sFR8052_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
667 (** val sFR8052_inv_rect_Type2 :
668 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
669 (__ -> 'a1) -> 'a1 **)
670 let sFR8052_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
671 let hcut = sFR8052_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
673 (** val sFR8052_inv_rect_Type1 :
674 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
675 (__ -> 'a1) -> 'a1 **)
676 let sFR8052_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
677 let hcut = sFR8052_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
679 (** val sFR8052_inv_rect_Type0 :
680 sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
681 (__ -> 'a1) -> 'a1 **)
682 let sFR8052_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
683 let hcut = sFR8052_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
685 (** val sFR8052_discr : sFR8052 -> sFR8052 -> __ **)
686 let sFR8052_discr x y =
687 Logic.eq_rect_Type2 x
689 | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
690 | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
691 | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
692 | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
693 | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
695 (** val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __ **)
696 let sFR8052_jmdiscr x y =
697 Logic.eq_rect_Type2 x
699 | SFR_T2CON -> Obj.magic (fun _ dH -> dH)
700 | SFR_RCAP2L -> Obj.magic (fun _ dH -> dH)
701 | SFR_RCAP2H -> Obj.magic (fun _ dH -> dH)
702 | SFR_TL2 -> Obj.magic (fun _ dH -> dH)
703 | SFR_TH2 -> Obj.magic (fun _ dH -> dH)) y
705 (** val sfr_8052_index : sFR8052 -> Nat.nat **)
706 let sfr_8052_index = function
708 | SFR_RCAP2L -> Nat.S Nat.O
709 | SFR_RCAP2H -> Nat.S (Nat.S Nat.O)
710 | SFR_TL2 -> Nat.S (Nat.S (Nat.S Nat.O))
711 | SFR_TH2 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
713 type 'm preStatus = { low_internal_ram : BitVector.byte
714 BitVectorTrie.bitVectorTrie;
715 high_internal_ram : BitVector.byte
716 BitVectorTrie.bitVectorTrie;
717 external_ram : BitVector.byte
718 BitVectorTrie.bitVectorTrie;
719 program_counter : BitVector.word;
720 special_function_registers_8051 : BitVector.byte
722 special_function_registers_8052 : BitVector.byte
724 p1_latch : BitVector.byte; p3_latch : BitVector.byte;
727 (** val preStatus_rect_Type4 :
728 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
729 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
730 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
731 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_510 =
734 let { low_internal_ram = low_internal_ram0; high_internal_ram =
735 high_internal_ram0; external_ram = external_ram0; program_counter =
736 program_counter0; special_function_registers_8051 =
737 special_function_registers_8053; special_function_registers_8052 =
738 special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
739 p3_latch0; clock = clock0 } = x_510
741 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
742 program_counter0 special_function_registers_8053
743 special_function_registers_8054 p1_latch0 p3_latch0 clock0
745 (** val preStatus_rect_Type5 :
746 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
747 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
748 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
749 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_512 =
752 let { low_internal_ram = low_internal_ram0; high_internal_ram =
753 high_internal_ram0; external_ram = external_ram0; program_counter =
754 program_counter0; special_function_registers_8051 =
755 special_function_registers_8053; special_function_registers_8052 =
756 special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
757 p3_latch0; clock = clock0 } = x_512
759 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
760 program_counter0 special_function_registers_8053
761 special_function_registers_8054 p1_latch0 p3_latch0 clock0
763 (** val preStatus_rect_Type3 :
764 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
765 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
766 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
767 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_514 =
770 let { low_internal_ram = low_internal_ram0; high_internal_ram =
771 high_internal_ram0; external_ram = external_ram0; program_counter =
772 program_counter0; special_function_registers_8051 =
773 special_function_registers_8053; special_function_registers_8052 =
774 special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
775 p3_latch0; clock = clock0 } = x_514
777 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
778 program_counter0 special_function_registers_8053
779 special_function_registers_8054 p1_latch0 p3_latch0 clock0
781 (** val preStatus_rect_Type2 :
782 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
783 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
784 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
785 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_516 =
788 let { low_internal_ram = low_internal_ram0; high_internal_ram =
789 high_internal_ram0; external_ram = external_ram0; program_counter =
790 program_counter0; special_function_registers_8051 =
791 special_function_registers_8053; special_function_registers_8052 =
792 special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
793 p3_latch0; clock = clock0 } = x_516
795 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
796 program_counter0 special_function_registers_8053
797 special_function_registers_8054 p1_latch0 p3_latch0 clock0
799 (** val preStatus_rect_Type1 :
800 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
801 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
802 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
803 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_518 =
806 let { low_internal_ram = low_internal_ram0; high_internal_ram =
807 high_internal_ram0; external_ram = external_ram0; program_counter =
808 program_counter0; special_function_registers_8051 =
809 special_function_registers_8053; special_function_registers_8052 =
810 special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
811 p3_latch0; clock = clock0 } = x_518
813 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
814 program_counter0 special_function_registers_8053
815 special_function_registers_8054 p1_latch0 p3_latch0 clock0
817 (** val preStatus_rect_Type0 :
818 'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
819 BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
820 -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
821 Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_520 =
824 let { low_internal_ram = low_internal_ram0; high_internal_ram =
825 high_internal_ram0; external_ram = external_ram0; program_counter =
826 program_counter0; special_function_registers_8051 =
827 special_function_registers_8053; special_function_registers_8052 =
828 special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
829 p3_latch0; clock = clock0 } = x_520
831 h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
832 program_counter0 special_function_registers_8053
833 special_function_registers_8054 p1_latch0 p3_latch0 clock0
835 (** val low_internal_ram :
836 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
837 let rec low_internal_ram code_memory xxx =
840 (** val high_internal_ram :
841 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
842 let rec high_internal_ram code_memory xxx =
843 xxx.high_internal_ram
845 (** val external_ram :
846 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie **)
847 let rec external_ram code_memory xxx =
850 (** val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word **)
851 let rec program_counter code_memory xxx =
854 (** val special_function_registers_8051 :
855 'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
856 let rec special_function_registers_8051 code_memory xxx =
857 xxx.special_function_registers_8051
859 (** val special_function_registers_8052 :
860 'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector **)
861 let rec special_function_registers_8052 code_memory xxx =
862 xxx.special_function_registers_8052
864 (** val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
865 let rec p1_latch code_memory xxx =
868 (** val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte **)
869 let rec p3_latch code_memory xxx =
872 (** val clock : 'a1 -> 'a1 preStatus -> time **)
873 let rec clock code_memory xxx =
876 (** val preStatus_inv_rect_Type4 :
877 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
878 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
879 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
880 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
881 BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
882 let preStatus_inv_rect_Type4 x2 hterm h1 =
883 let hcut = preStatus_rect_Type4 x2 h1 hterm in hcut __
885 (** val preStatus_inv_rect_Type3 :
886 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
887 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
888 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
889 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
890 BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
891 let preStatus_inv_rect_Type3 x2 hterm h1 =
892 let hcut = preStatus_rect_Type3 x2 h1 hterm in hcut __
894 (** val preStatus_inv_rect_Type2 :
895 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
896 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
897 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
898 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
899 BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
900 let preStatus_inv_rect_Type2 x2 hterm h1 =
901 let hcut = preStatus_rect_Type2 x2 h1 hterm in hcut __
903 (** val preStatus_inv_rect_Type1 :
904 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
905 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
906 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
907 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
908 BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
909 let preStatus_inv_rect_Type1 x2 hterm h1 =
910 let hcut = preStatus_rect_Type1 x2 h1 hterm in hcut __
912 (** val preStatus_inv_rect_Type0 :
913 'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
914 BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
915 BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
916 Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
917 BitVector.byte -> time -> __ -> 'a2) -> 'a2 **)
918 let preStatus_inv_rect_Type0 x2 hterm h1 =
919 let hcut = preStatus_rect_Type0 x2 h1 hterm in hcut __
921 (** val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __ **)
922 let preStatus_jmdiscr a2 x y =
923 Logic.eq_rect_Type2 x
924 (let { low_internal_ram = a0; high_internal_ram = a10; external_ram =
925 a20; program_counter = a3; special_function_registers_8051 = a4;
926 special_function_registers_8052 = a5; p1_latch = a6; p3_latch = a7;
929 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
931 type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
933 type pseudoStatus = ASM.pseudo_assembly_program preStatus
935 (** val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus **)
936 let set_clock code_memory s t =
937 let old_low_internal_ram = s.low_internal_ram in
938 let old_high_internal_ram = s.high_internal_ram in
939 let old_external_ram = s.external_ram in
940 let old_program_counter = s.program_counter in
941 let old_special_function_registers_8051 = s.special_function_registers_8051
943 let old_special_function_registers_8052 = s.special_function_registers_8052
945 let old_p1_latch = s.p1_latch in
946 let old_p3_latch = s.p3_latch in
947 { low_internal_ram = old_low_internal_ram; high_internal_ram =
948 old_high_internal_ram; external_ram = old_external_ram; program_counter =
949 old_program_counter; special_function_registers_8051 =
950 old_special_function_registers_8051; special_function_registers_8052 =
951 old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
952 old_p3_latch; clock = t }
954 (** val set_p1_latch :
955 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
956 let set_p1_latch code_memory s b =
957 let old_low_internal_ram = s.low_internal_ram in
958 let old_high_internal_ram = s.high_internal_ram in
959 let old_external_ram = s.external_ram in
960 let old_program_counter = s.program_counter in
961 let old_special_function_registers_8051 = s.special_function_registers_8051
963 let old_special_function_registers_8052 = s.special_function_registers_8052
965 let old_p3_latch = s.p3_latch in
966 let old_clock = s.clock in
967 { low_internal_ram = old_low_internal_ram; high_internal_ram =
968 old_high_internal_ram; external_ram = old_external_ram; program_counter =
969 old_program_counter; special_function_registers_8051 =
970 old_special_function_registers_8051; special_function_registers_8052 =
971 old_special_function_registers_8052; p1_latch = b; p3_latch = old_p3_latch;
974 (** val set_p3_latch :
975 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
976 let set_p3_latch code_memory s b =
977 let old_low_internal_ram = s.low_internal_ram in
978 let old_high_internal_ram = s.high_internal_ram in
979 let old_external_ram = s.external_ram in
980 let old_program_counter = s.program_counter in
981 let old_special_function_registers_8051 = s.special_function_registers_8051
983 let old_special_function_registers_8052 = s.special_function_registers_8052
985 let old_p1_latch = s.p1_latch in
986 let old_clock = s.clock in
987 { low_internal_ram = old_low_internal_ram; high_internal_ram =
988 old_high_internal_ram; external_ram = old_external_ram; program_counter =
989 old_program_counter; special_function_registers_8051 =
990 old_special_function_registers_8051; special_function_registers_8052 =
991 old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch = b;
994 (** val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte **)
995 let get_8051_sfr code_memory s i =
996 let sfr = s.special_function_registers_8051 in
997 let index = sfr_8051_index i in
998 Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
999 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1000 (Nat.S Nat.O))))))))))))))))))) sfr index
1002 (** val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte **)
1003 let get_8052_sfr code_memory s i =
1004 let sfr = s.special_function_registers_8052 in
1005 let index = sfr_8052_index i in
1006 Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) sfr index
1008 (** val set_8051_sfr :
1009 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus **)
1010 let set_8051_sfr code_memory s i b =
1011 let index = sfr_8051_index i in
1012 let old_low_internal_ram = s.low_internal_ram in
1013 let old_high_internal_ram = s.high_internal_ram in
1014 let old_external_ram = s.external_ram in
1015 let old_program_counter = s.program_counter in
1016 let old_special_function_registers_8051 = s.special_function_registers_8051
1018 let old_special_function_registers_8052 = s.special_function_registers_8052
1020 let new_special_function_registers_8051 =
1021 Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1022 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1023 (Nat.S Nat.O))))))))))))))))))) old_special_function_registers_8051
1026 let old_p1_latch = s.p1_latch in
1027 let old_p3_latch = s.p3_latch in
1028 let old_clock = s.clock in
1029 { low_internal_ram = old_low_internal_ram; high_internal_ram =
1030 old_high_internal_ram; external_ram = old_external_ram; program_counter =
1031 old_program_counter; special_function_registers_8051 =
1032 new_special_function_registers_8051; special_function_registers_8052 =
1033 old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1034 old_p3_latch; clock = old_clock }
1036 (** val set_8052_sfr :
1037 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus **)
1038 let set_8052_sfr code_memory s i b =
1039 let index = sfr_8052_index i in
1040 let old_low_internal_ram = s.low_internal_ram in
1041 let old_high_internal_ram = s.high_internal_ram in
1042 let old_external_ram = s.external_ram in
1043 let old_program_counter = s.program_counter in
1044 let old_special_function_registers_8051 = s.special_function_registers_8051
1046 let old_special_function_registers_8052 = s.special_function_registers_8052
1048 let new_special_function_registers_8052 =
1049 Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1050 old_special_function_registers_8052 index b
1052 let old_p1_latch = s.p1_latch in
1053 let old_p3_latch = s.p3_latch in
1054 let old_clock = s.clock in
1055 { low_internal_ram = old_low_internal_ram; high_internal_ram =
1056 old_high_internal_ram; external_ram = old_external_ram; program_counter =
1057 old_program_counter; special_function_registers_8051 =
1058 old_special_function_registers_8051; special_function_registers_8052 =
1059 new_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1060 old_p3_latch; clock = old_clock }
1062 (** val set_program_counter :
1063 'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus **)
1064 let set_program_counter code_memory s w =
1065 let old_low_internal_ram = s.low_internal_ram in
1066 let old_high_internal_ram = s.high_internal_ram in
1067 let old_external_ram = s.external_ram in
1068 let old_special_function_registers_8051 = s.special_function_registers_8051
1070 let old_special_function_registers_8052 = s.special_function_registers_8052
1072 let old_p1_latch = s.p1_latch in
1073 let old_p3_latch = s.p3_latch in
1074 let old_clock = s.clock in
1075 { low_internal_ram = old_low_internal_ram; high_internal_ram =
1076 old_high_internal_ram; external_ram = old_external_ram; program_counter =
1077 w; special_function_registers_8051 = old_special_function_registers_8051;
1078 special_function_registers_8052 = old_special_function_registers_8052;
1079 p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1081 (** val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus **)
1082 let set_code_memory code_memory s r =
1083 let old_low_internal_ram = s.low_internal_ram in
1084 let old_high_internal_ram = s.high_internal_ram in
1085 let old_external_ram = s.external_ram in
1086 let old_program_counter = s.program_counter in
1087 let old_special_function_registers_8051 = s.special_function_registers_8051
1089 let old_special_function_registers_8052 = s.special_function_registers_8052
1091 let old_p1_latch = s.p1_latch in
1092 let old_p3_latch = s.p3_latch in
1093 let old_clock = s.clock in
1094 { low_internal_ram = old_low_internal_ram; high_internal_ram =
1095 old_high_internal_ram; external_ram = old_external_ram; program_counter =
1096 old_program_counter; special_function_registers_8051 =
1097 old_special_function_registers_8051; special_function_registers_8052 =
1098 old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1099 old_p3_latch; clock = old_clock }
1101 (** val set_low_internal_ram :
1102 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1104 let set_low_internal_ram code_memory s r =
1105 let old_high_internal_ram = s.high_internal_ram in
1106 let old_external_ram = s.external_ram in
1107 let old_program_counter = s.program_counter in
1108 let old_special_function_registers_8051 = s.special_function_registers_8051
1110 let old_special_function_registers_8052 = s.special_function_registers_8052
1112 let old_p1_latch = s.p1_latch in
1113 let old_p3_latch = s.p3_latch in
1114 let old_clock = s.clock in
1115 { low_internal_ram = r; high_internal_ram = old_high_internal_ram;
1116 external_ram = old_external_ram; program_counter = old_program_counter;
1117 special_function_registers_8051 = old_special_function_registers_8051;
1118 special_function_registers_8052 = old_special_function_registers_8052;
1119 p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1121 (** val update_low_internal_ram :
1122 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1124 let update_low_internal_ram code_memory s addr v =
1125 let old_low_internal_ram = s.low_internal_ram in
1126 let new_low_internal_ram =
1127 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1128 Nat.O))))))) addr v old_low_internal_ram
1130 set_low_internal_ram code_memory s new_low_internal_ram
1132 (** val set_high_internal_ram :
1133 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1135 let set_high_internal_ram code_memory s r =
1136 let old_low_internal_ram = s.low_internal_ram in
1137 let old_high_internal_ram = s.high_internal_ram in
1138 let old_external_ram = s.external_ram in
1139 let old_program_counter = s.program_counter in
1140 let old_special_function_registers_8051 = s.special_function_registers_8051
1142 let old_special_function_registers_8052 = s.special_function_registers_8052
1144 let old_p1_latch = s.p1_latch in
1145 let old_p3_latch = s.p3_latch in
1146 let old_clock = s.clock in
1147 { low_internal_ram = old_low_internal_ram; high_internal_ram = r;
1148 external_ram = old_external_ram; program_counter = old_program_counter;
1149 special_function_registers_8051 = old_special_function_registers_8051;
1150 special_function_registers_8052 = old_special_function_registers_8052;
1151 p1_latch = old_p1_latch; p3_latch = old_p3_latch; clock = old_clock }
1153 (** val update_high_internal_ram :
1154 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1156 let update_high_internal_ram code_memory s addr v =
1157 let old_high_internal_ram = s.high_internal_ram in
1158 let new_high_internal_ram =
1159 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1160 Nat.O))))))) addr v old_high_internal_ram
1162 set_high_internal_ram code_memory s new_high_internal_ram
1164 (** val set_external_ram :
1165 'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
1167 let set_external_ram code_memory s r =
1168 let old_low_internal_ram = s.low_internal_ram in
1169 let old_high_internal_ram = s.high_internal_ram in
1170 let old_program_counter = s.program_counter in
1171 let old_special_function_registers_8051 = s.special_function_registers_8051
1173 let old_special_function_registers_8052 = s.special_function_registers_8052
1175 let old_p1_latch = s.p1_latch in
1176 let old_p3_latch = s.p3_latch in
1177 let old_clock = s.clock in
1178 { low_internal_ram = old_low_internal_ram; high_internal_ram =
1179 old_high_internal_ram; external_ram = r; program_counter =
1180 old_program_counter; special_function_registers_8051 =
1181 old_special_function_registers_8051; special_function_registers_8052 =
1182 old_special_function_registers_8052; p1_latch = old_p1_latch; p3_latch =
1183 old_p3_latch; clock = old_clock }
1185 (** val update_external_ram :
1186 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
1188 let update_external_ram code_memory s addr v =
1189 let old_external_ram = s.external_ram in
1190 let new_external_ram =
1191 BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1192 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1193 Nat.O)))))))))))))))) addr v old_external_ram
1195 set_external_ram code_memory s new_external_ram
1197 (** val get_psw_flags : 'a1 -> 'a1 preStatus -> Nat.nat -> Bool.bool **)
1198 let get_psw_flags code_memory s flag =
1199 let psw = get_8051_sfr code_memory s SFR_PSW in
1200 Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1201 Nat.O)))))))) psw flag
1203 (** val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1204 let get_cy_flag code_memory s =
1205 get_psw_flags code_memory s Nat.O
1207 (** val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1208 let get_ac_flag code_memory s =
1209 get_psw_flags code_memory s (Nat.S Nat.O)
1211 (** val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1212 let get_fo_flag code_memory s =
1213 get_psw_flags code_memory s (Nat.S (Nat.S Nat.O))
1215 (** val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1216 let get_rs1_flag code_memory s =
1217 get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S Nat.O)))
1219 (** val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1220 let get_rs0_flag code_memory s =
1221 get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1223 (** val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1224 let get_ov_flag code_memory s =
1225 get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1227 (** val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1228 let get_ud_flag code_memory s =
1229 get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1232 (** val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool **)
1233 let get_p_flag code_memory s =
1234 get_psw_flags code_memory s (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1238 'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
1239 BitVector.bit -> 'a1 preStatus **)
1240 let set_flags code_memory s cy ac ov =
1241 let old_cy = get_cy_flag code_memory s in
1242 let old_ac = get_ac_flag code_memory s in
1243 let old_fo = get_fo_flag code_memory s in
1244 let old_rs1 = get_rs1_flag code_memory s in
1245 let old_rs0 = get_rs0_flag code_memory s in
1246 let old_ov = get_ov_flag code_memory s in
1247 let old_ud = get_ud_flag code_memory s in
1248 let old_p = get_p_flag code_memory s in
1251 | Types.None -> old_ac
1254 set_8051_sfr code_memory s SFR_PSW (Vector.VCons ((Nat.S (Nat.S (Nat.S
1255 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), cy, (Vector.VCons ((Nat.S
1256 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), new_ac, (Vector.VCons
1257 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), old_fo, (Vector.VCons
1258 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), old_rs1, (Vector.VCons ((Nat.S
1259 (Nat.S (Nat.S Nat.O))), old_rs0, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1260 ov, (Vector.VCons ((Nat.S Nat.O), old_ud, (Vector.VCons (Nat.O, old_p,
1261 Vector.VEmpty))))))))))))))))
1263 (** val initialise_status : 'a1 -> 'a1 preStatus **)
1264 let initialise_status code_mem =
1265 let status0 = { low_internal_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1266 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))); high_internal_ram =
1267 (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1268 Nat.O)))))))); external_ram = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S
1269 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1270 (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))); program_counter =
1271 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1272 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1273 Nat.O))))))))))))))))); special_function_registers_8051 =
1274 (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1275 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1276 (Nat.S Nat.O)))))))))))))))))))
1277 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1278 Nat.O)))))))))); special_function_registers_8052 =
1279 (Vector.replicate (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1280 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1281 Nat.O)))))))))); p1_latch =
1282 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1283 Nat.O))))))))); p3_latch =
1284 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1285 Nat.O))))))))); clock = Nat.O }
1287 set_8051_sfr code_mem status0 SFR_SP
1288 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1289 (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1290 (Nat.S Nat.O))))))))
1292 (** val sfr_of_Byte :
1293 BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option **)
1296 Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1297 (Nat.S (Nat.S Nat.O)))))))) b
1299 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1300 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1301 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1302 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1303 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1304 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1305 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1306 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1307 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1308 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1309 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1310 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1311 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1312 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1313 (Nat.S (Nat.S (Nat.S (Nat.S
1314 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1315 | Bool.True -> Types.None
1317 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1318 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1319 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1320 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1321 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1322 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1323 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1324 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1325 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1326 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1327 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1328 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1329 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1330 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1331 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1332 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1334 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1335 | Bool.True -> Types.Some (Types.Inl SFR_P1)
1337 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1338 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1339 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1340 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1341 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1342 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1343 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1344 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1345 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1346 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1347 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1348 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1349 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1350 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1351 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1352 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1354 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1355 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1356 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1358 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1359 | Bool.True -> Types.None
1361 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1362 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1363 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1364 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1365 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1366 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1367 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1368 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1369 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1370 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1371 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1372 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1373 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1374 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1375 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1376 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1377 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1378 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1379 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1380 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1381 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1382 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1384 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1385 | Bool.True -> Types.Some (Types.Inl SFR_P3)
1387 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1388 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1389 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1390 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1391 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1392 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1393 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1394 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1395 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1396 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1397 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1398 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1399 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1400 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1401 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1402 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1403 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1404 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1405 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1406 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1407 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1408 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1410 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1411 | Bool.True -> Types.Some (Types.Inl SFR_SBUF)
1413 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1414 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1415 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1416 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1417 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1418 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1419 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1420 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1421 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1422 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1423 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1424 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1425 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1426 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1427 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1428 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1429 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1430 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1431 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1432 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1433 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1434 | Bool.True -> Types.Some (Types.Inl SFR_TL0)
1436 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1437 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1438 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1439 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1440 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1441 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1442 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1443 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1444 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1445 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1446 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1447 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1448 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1449 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1450 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1451 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1452 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1453 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1454 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1455 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1457 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1458 | Bool.True -> Types.Some (Types.Inl SFR_TL1)
1460 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1461 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1462 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1463 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1464 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1465 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1466 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1467 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1468 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1469 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1470 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1471 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1472 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1473 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1474 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1475 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1476 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1477 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1478 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1479 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1480 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1481 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1482 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1483 (Nat.S (Nat.S (Nat.S (Nat.S
1484 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1485 | Bool.True -> Types.Some (Types.Inl SFR_TH0)
1487 (match Nat.eqb address (Nat.S (Nat.S (Nat.S (Nat.S
1488 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1489 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1490 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1491 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1492 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1493 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1494 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1495 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1496 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1497 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1498 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1499 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1500 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1501 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1502 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1503 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1504 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1505 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1506 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1507 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1508 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1509 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1510 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1511 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1512 | Bool.True -> Types.Some (Types.Inl SFR_TH1)
1514 (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1515 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1516 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1517 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1518 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1519 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1520 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1521 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1522 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1523 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1524 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1525 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1526 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1527 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1528 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1529 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1530 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1531 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1532 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1533 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1534 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1535 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1536 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1537 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1538 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1539 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1540 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1541 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1542 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1543 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1544 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1545 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1546 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1547 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1548 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1549 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1550 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1551 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1552 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1553 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1555 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1556 | Bool.True -> Types.Some (Types.Inr SFR_T2CON)
1558 (match Nat.eqb address (Nat.S (Nat.S (Nat.S
1559 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1560 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1561 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1562 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1563 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1564 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1565 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1566 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1567 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1568 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1569 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1570 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1571 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1572 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1573 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1574 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1575 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1576 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1577 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1578 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1579 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1580 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1581 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1582 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1583 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1584 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1585 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1586 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1587 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1588 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1589 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1590 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1591 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1592 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1593 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1594 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1595 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1597 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1598 (Nat.S (Nat.S (Nat.S (Nat.S
1599 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1601 Types.Some (Types.Inr SFR_RCAP2L)
1603 (match Nat.eqb address (Nat.S (Nat.S
1604 (Nat.S (Nat.S (Nat.S (Nat.S
1605 (Nat.S (Nat.S (Nat.S (Nat.S
1606 (Nat.S (Nat.S (Nat.S (Nat.S
1607 (Nat.S (Nat.S (Nat.S (Nat.S
1608 (Nat.S (Nat.S (Nat.S (Nat.S
1609 (Nat.S (Nat.S (Nat.S (Nat.S
1610 (Nat.S (Nat.S (Nat.S (Nat.S
1611 (Nat.S (Nat.S (Nat.S (Nat.S
1612 (Nat.S (Nat.S (Nat.S (Nat.S
1613 (Nat.S (Nat.S (Nat.S (Nat.S
1614 (Nat.S (Nat.S (Nat.S (Nat.S
1615 (Nat.S (Nat.S (Nat.S (Nat.S
1616 (Nat.S (Nat.S (Nat.S (Nat.S
1617 (Nat.S (Nat.S (Nat.S (Nat.S
1618 (Nat.S (Nat.S (Nat.S (Nat.S
1619 (Nat.S (Nat.S (Nat.S (Nat.S
1620 (Nat.S (Nat.S (Nat.S (Nat.S
1621 (Nat.S (Nat.S (Nat.S (Nat.S
1622 (Nat.S (Nat.S (Nat.S (Nat.S
1623 (Nat.S (Nat.S (Nat.S (Nat.S
1624 (Nat.S (Nat.S (Nat.S (Nat.S
1625 (Nat.S (Nat.S (Nat.S (Nat.S
1626 (Nat.S (Nat.S (Nat.S (Nat.S
1627 (Nat.S (Nat.S (Nat.S (Nat.S
1628 (Nat.S (Nat.S (Nat.S (Nat.S
1629 (Nat.S (Nat.S (Nat.S (Nat.S
1630 (Nat.S (Nat.S (Nat.S (Nat.S
1631 (Nat.S (Nat.S (Nat.S (Nat.S
1632 (Nat.S (Nat.S (Nat.S (Nat.S
1633 (Nat.S (Nat.S (Nat.S (Nat.S
1634 (Nat.S (Nat.S (Nat.S (Nat.S
1635 (Nat.S (Nat.S (Nat.S (Nat.S
1636 (Nat.S (Nat.S (Nat.S (Nat.S
1637 (Nat.S (Nat.S (Nat.S (Nat.S
1638 (Nat.S (Nat.S (Nat.S (Nat.S
1639 (Nat.S (Nat.S (Nat.S (Nat.S
1640 (Nat.S (Nat.S (Nat.S (Nat.S
1641 (Nat.S (Nat.S (Nat.S (Nat.S
1642 (Nat.S (Nat.S (Nat.S (Nat.S
1643 (Nat.S (Nat.S (Nat.S (Nat.S
1644 (Nat.S (Nat.S (Nat.S (Nat.S
1645 (Nat.S (Nat.S (Nat.S (Nat.S
1646 (Nat.S (Nat.S (Nat.S (Nat.S
1647 (Nat.S (Nat.S (Nat.S (Nat.S
1648 (Nat.S (Nat.S (Nat.S (Nat.S
1649 (Nat.S (Nat.S (Nat.S (Nat.S
1650 (Nat.S (Nat.S (Nat.S (Nat.S
1651 (Nat.S (Nat.S (Nat.S (Nat.S
1652 (Nat.S (Nat.S (Nat.S (Nat.S
1653 (Nat.S (Nat.S (Nat.S (Nat.S
1655 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1657 Types.Some (Types.Inr SFR_RCAP2H)
1659 (match Nat.eqb address (Nat.S (Nat.S
1660 (Nat.S (Nat.S (Nat.S (Nat.S
1661 (Nat.S (Nat.S (Nat.S (Nat.S
1662 (Nat.S (Nat.S (Nat.S (Nat.S
1663 (Nat.S (Nat.S (Nat.S (Nat.S
1664 (Nat.S (Nat.S (Nat.S (Nat.S
1665 (Nat.S (Nat.S (Nat.S (Nat.S
1666 (Nat.S (Nat.S (Nat.S (Nat.S
1667 (Nat.S (Nat.S (Nat.S (Nat.S
1668 (Nat.S (Nat.S (Nat.S (Nat.S
1669 (Nat.S (Nat.S (Nat.S (Nat.S
1670 (Nat.S (Nat.S (Nat.S (Nat.S
1671 (Nat.S (Nat.S (Nat.S (Nat.S
1672 (Nat.S (Nat.S (Nat.S (Nat.S
1673 (Nat.S (Nat.S (Nat.S (Nat.S
1674 (Nat.S (Nat.S (Nat.S (Nat.S
1675 (Nat.S (Nat.S (Nat.S (Nat.S
1676 (Nat.S (Nat.S (Nat.S (Nat.S
1677 (Nat.S (Nat.S (Nat.S (Nat.S
1678 (Nat.S (Nat.S (Nat.S (Nat.S
1679 (Nat.S (Nat.S (Nat.S (Nat.S
1680 (Nat.S (Nat.S (Nat.S (Nat.S
1681 (Nat.S (Nat.S (Nat.S (Nat.S
1682 (Nat.S (Nat.S (Nat.S (Nat.S
1683 (Nat.S (Nat.S (Nat.S (Nat.S
1684 (Nat.S (Nat.S (Nat.S (Nat.S
1685 (Nat.S (Nat.S (Nat.S (Nat.S
1686 (Nat.S (Nat.S (Nat.S (Nat.S
1687 (Nat.S (Nat.S (Nat.S (Nat.S
1688 (Nat.S (Nat.S (Nat.S (Nat.S
1689 (Nat.S (Nat.S (Nat.S (Nat.S
1690 (Nat.S (Nat.S (Nat.S (Nat.S
1691 (Nat.S (Nat.S (Nat.S (Nat.S
1692 (Nat.S (Nat.S (Nat.S (Nat.S
1693 (Nat.S (Nat.S (Nat.S (Nat.S
1694 (Nat.S (Nat.S (Nat.S (Nat.S
1695 (Nat.S (Nat.S (Nat.S (Nat.S
1696 (Nat.S (Nat.S (Nat.S (Nat.S
1697 (Nat.S (Nat.S (Nat.S (Nat.S
1698 (Nat.S (Nat.S (Nat.S (Nat.S
1699 (Nat.S (Nat.S (Nat.S (Nat.S
1700 (Nat.S (Nat.S (Nat.S (Nat.S
1701 (Nat.S (Nat.S (Nat.S (Nat.S
1702 (Nat.S (Nat.S (Nat.S (Nat.S
1703 (Nat.S (Nat.S (Nat.S (Nat.S
1704 (Nat.S (Nat.S (Nat.S (Nat.S
1705 (Nat.S (Nat.S (Nat.S (Nat.S
1706 (Nat.S (Nat.S (Nat.S (Nat.S
1707 (Nat.S (Nat.S (Nat.S (Nat.S
1708 (Nat.S (Nat.S (Nat.S (Nat.S
1709 (Nat.S (Nat.S (Nat.S (Nat.S
1711 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1713 Types.Some (Types.Inr SFR_TL2)
1715 (match Nat.eqb address (Nat.S (Nat.S
1716 (Nat.S (Nat.S (Nat.S (Nat.S
1717 (Nat.S (Nat.S (Nat.S (Nat.S
1718 (Nat.S (Nat.S (Nat.S (Nat.S
1719 (Nat.S (Nat.S (Nat.S (Nat.S
1720 (Nat.S (Nat.S (Nat.S (Nat.S
1721 (Nat.S (Nat.S (Nat.S (Nat.S
1722 (Nat.S (Nat.S (Nat.S (Nat.S
1723 (Nat.S (Nat.S (Nat.S (Nat.S
1724 (Nat.S (Nat.S (Nat.S (Nat.S
1725 (Nat.S (Nat.S (Nat.S (Nat.S
1726 (Nat.S (Nat.S (Nat.S (Nat.S
1727 (Nat.S (Nat.S (Nat.S (Nat.S
1728 (Nat.S (Nat.S (Nat.S (Nat.S
1729 (Nat.S (Nat.S (Nat.S (Nat.S
1730 (Nat.S (Nat.S (Nat.S (Nat.S
1731 (Nat.S (Nat.S (Nat.S (Nat.S
1732 (Nat.S (Nat.S (Nat.S (Nat.S
1733 (Nat.S (Nat.S (Nat.S (Nat.S
1734 (Nat.S (Nat.S (Nat.S (Nat.S
1735 (Nat.S (Nat.S (Nat.S (Nat.S
1736 (Nat.S (Nat.S (Nat.S (Nat.S
1737 (Nat.S (Nat.S (Nat.S (Nat.S
1738 (Nat.S (Nat.S (Nat.S (Nat.S
1739 (Nat.S (Nat.S (Nat.S (Nat.S
1740 (Nat.S (Nat.S (Nat.S (Nat.S
1741 (Nat.S (Nat.S (Nat.S (Nat.S
1742 (Nat.S (Nat.S (Nat.S (Nat.S
1743 (Nat.S (Nat.S (Nat.S (Nat.S
1744 (Nat.S (Nat.S (Nat.S (Nat.S
1745 (Nat.S (Nat.S (Nat.S (Nat.S
1746 (Nat.S (Nat.S (Nat.S (Nat.S
1747 (Nat.S (Nat.S (Nat.S (Nat.S
1748 (Nat.S (Nat.S (Nat.S (Nat.S
1749 (Nat.S (Nat.S (Nat.S (Nat.S
1750 (Nat.S (Nat.S (Nat.S (Nat.S
1751 (Nat.S (Nat.S (Nat.S (Nat.S
1752 (Nat.S (Nat.S (Nat.S (Nat.S
1753 (Nat.S (Nat.S (Nat.S (Nat.S
1754 (Nat.S (Nat.S (Nat.S (Nat.S
1755 (Nat.S (Nat.S (Nat.S (Nat.S
1756 (Nat.S (Nat.S (Nat.S (Nat.S
1757 (Nat.S (Nat.S (Nat.S (Nat.S
1758 (Nat.S (Nat.S (Nat.S (Nat.S
1759 (Nat.S (Nat.S (Nat.S (Nat.S
1760 (Nat.S (Nat.S (Nat.S (Nat.S
1761 (Nat.S (Nat.S (Nat.S (Nat.S
1762 (Nat.S (Nat.S (Nat.S (Nat.S
1763 (Nat.S (Nat.S (Nat.S (Nat.S
1764 (Nat.S (Nat.S (Nat.S (Nat.S
1765 (Nat.S (Nat.S (Nat.S (Nat.S
1766 (Nat.S (Nat.S (Nat.S
1767 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1769 Types.Some (Types.Inr SFR_TH2)
1771 (match Nat.eqb address (Nat.S
1772 (Nat.S (Nat.S (Nat.S
1773 (Nat.S (Nat.S (Nat.S
1774 (Nat.S (Nat.S (Nat.S
1775 (Nat.S (Nat.S (Nat.S
1776 (Nat.S (Nat.S (Nat.S
1777 (Nat.S (Nat.S (Nat.S
1778 (Nat.S (Nat.S (Nat.S
1779 (Nat.S (Nat.S (Nat.S
1780 (Nat.S (Nat.S (Nat.S
1781 (Nat.S (Nat.S (Nat.S
1782 (Nat.S (Nat.S (Nat.S
1783 (Nat.S (Nat.S (Nat.S
1784 (Nat.S (Nat.S (Nat.S
1785 (Nat.S (Nat.S (Nat.S
1786 (Nat.S (Nat.S (Nat.S
1787 (Nat.S (Nat.S (Nat.S
1788 (Nat.S (Nat.S (Nat.S
1789 (Nat.S (Nat.S (Nat.S
1790 (Nat.S (Nat.S (Nat.S
1791 (Nat.S (Nat.S (Nat.S
1792 (Nat.S (Nat.S (Nat.S
1793 (Nat.S (Nat.S (Nat.S
1794 (Nat.S (Nat.S (Nat.S
1795 (Nat.S (Nat.S (Nat.S
1796 (Nat.S (Nat.S (Nat.S
1797 (Nat.S (Nat.S (Nat.S
1798 (Nat.S (Nat.S (Nat.S
1799 (Nat.S (Nat.S (Nat.S
1800 (Nat.S (Nat.S (Nat.S
1801 (Nat.S (Nat.S (Nat.S
1802 (Nat.S (Nat.S (Nat.S
1803 (Nat.S (Nat.S (Nat.S
1804 (Nat.S (Nat.S (Nat.S
1805 (Nat.S (Nat.S (Nat.S
1806 (Nat.S (Nat.S (Nat.S
1807 (Nat.S (Nat.S (Nat.S
1808 (Nat.S (Nat.S (Nat.S
1809 (Nat.S (Nat.S (Nat.S
1810 (Nat.S (Nat.S (Nat.S
1811 (Nat.S (Nat.S (Nat.S
1812 (Nat.S (Nat.S (Nat.S
1813 (Nat.S (Nat.S (Nat.S
1814 (Nat.S (Nat.S (Nat.S
1815 (Nat.S (Nat.S (Nat.S
1817 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1819 Types.Some (Types.Inl
1822 (match Nat.eqb address (Nat.S
1823 (Nat.S (Nat.S (Nat.S
1824 (Nat.S (Nat.S (Nat.S
1825 (Nat.S (Nat.S (Nat.S
1826 (Nat.S (Nat.S (Nat.S
1827 (Nat.S (Nat.S (Nat.S
1828 (Nat.S (Nat.S (Nat.S
1829 (Nat.S (Nat.S (Nat.S
1830 (Nat.S (Nat.S (Nat.S
1831 (Nat.S (Nat.S (Nat.S
1832 (Nat.S (Nat.S (Nat.S
1833 (Nat.S (Nat.S (Nat.S
1834 (Nat.S (Nat.S (Nat.S
1835 (Nat.S (Nat.S (Nat.S
1836 (Nat.S (Nat.S (Nat.S
1837 (Nat.S (Nat.S (Nat.S
1838 (Nat.S (Nat.S (Nat.S
1839 (Nat.S (Nat.S (Nat.S
1840 (Nat.S (Nat.S (Nat.S
1841 (Nat.S (Nat.S (Nat.S
1842 (Nat.S (Nat.S (Nat.S
1843 (Nat.S (Nat.S (Nat.S
1844 (Nat.S (Nat.S (Nat.S
1845 (Nat.S (Nat.S (Nat.S
1846 (Nat.S (Nat.S (Nat.S
1847 (Nat.S (Nat.S (Nat.S
1848 (Nat.S (Nat.S (Nat.S
1849 (Nat.S (Nat.S (Nat.S
1850 (Nat.S (Nat.S (Nat.S
1851 (Nat.S (Nat.S (Nat.S
1852 (Nat.S (Nat.S (Nat.S
1853 (Nat.S (Nat.S (Nat.S
1854 (Nat.S (Nat.S (Nat.S
1855 (Nat.S (Nat.S (Nat.S
1856 (Nat.S (Nat.S (Nat.S
1857 (Nat.S (Nat.S (Nat.S
1858 (Nat.S (Nat.S (Nat.S
1859 (Nat.S (Nat.S (Nat.S
1860 (Nat.S (Nat.S (Nat.S
1861 (Nat.S (Nat.S (Nat.S
1862 (Nat.S (Nat.S (Nat.S
1863 (Nat.S (Nat.S (Nat.S
1864 (Nat.S (Nat.S (Nat.S
1865 (Nat.S (Nat.S (Nat.S
1866 (Nat.S (Nat.S (Nat.S
1867 (Nat.S (Nat.S (Nat.S
1868 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1870 Types.Some (Types.Inl
1873 (match Nat.eqb address
1943 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
1945 Types.Some (Types.Inl
1948 (match Nat.eqb address
2025 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2027 Types.Some (Types.Inl
2200 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2392 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2530 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2669 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
2809 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3026 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3259 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3508 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) with
3514 Types.None))))))))))))))))))))))))))
3516 (** val get_bit_addressable_sfr :
3517 'a1 -> 'a1 preStatus -> BitVector.byte -> Bool.bool -> BitVector.byte **)
3518 let get_bit_addressable_sfr code_memory s b l =
3519 match sfr_of_Byte b with
3520 | Types.None -> assert false (* absurd case *)
3521 | Types.Some sfr8051_8052 ->
3522 (match sfr8051_8052 with
3525 | SFR_SP -> get_8051_sfr code_memory s sfr
3526 | SFR_DPL -> get_8051_sfr code_memory s sfr
3527 | SFR_DPH -> get_8051_sfr code_memory s sfr
3528 | SFR_PCON -> get_8051_sfr code_memory s sfr
3529 | SFR_TCON -> get_8051_sfr code_memory s sfr
3530 | SFR_TMOD -> get_8051_sfr code_memory s sfr
3531 | SFR_TL0 -> get_8051_sfr code_memory s sfr
3532 | SFR_TL1 -> get_8051_sfr code_memory s sfr
3533 | SFR_TH0 -> get_8051_sfr code_memory s sfr
3534 | SFR_TH1 -> get_8051_sfr code_memory s sfr
3537 | Bool.True -> s.p1_latch
3538 | Bool.False -> get_8051_sfr code_memory s SFR_P1)
3539 | SFR_SCON -> get_8051_sfr code_memory s sfr
3540 | SFR_SBUF -> get_8051_sfr code_memory s sfr
3541 | SFR_IE -> get_8051_sfr code_memory s sfr
3544 | Bool.True -> s.p3_latch
3545 | Bool.False -> get_8051_sfr code_memory s SFR_P3)
3546 | SFR_IP -> get_8051_sfr code_memory s sfr
3547 | SFR_PSW -> get_8051_sfr code_memory s sfr
3548 | SFR_ACC_A -> get_8051_sfr code_memory s sfr
3549 | SFR_ACC_B -> get_8051_sfr code_memory s sfr)
3550 | Types.Inr sfr -> get_8052_sfr code_memory s sfr)
3552 (** val set_bit_addressable_sfr :
3553 'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte -> 'a1 preStatus **)
3554 let set_bit_addressable_sfr code_memory s b v =
3555 match sfr_of_Byte b with
3556 | Types.None -> assert false (* absurd case *)
3557 | Types.Some sfr8051_8052 ->
3558 (match sfr8051_8052 with
3561 | SFR_SP -> set_8051_sfr code_memory s sfr v
3562 | SFR_DPL -> set_8051_sfr code_memory s sfr v
3563 | SFR_DPH -> set_8051_sfr code_memory s sfr v
3564 | SFR_PCON -> set_8051_sfr code_memory s sfr v
3565 | SFR_TCON -> set_8051_sfr code_memory s sfr v
3566 | SFR_TMOD -> set_8051_sfr code_memory s sfr v
3567 | SFR_TL0 -> set_8051_sfr code_memory s sfr v
3568 | SFR_TL1 -> set_8051_sfr code_memory s sfr v
3569 | SFR_TH0 -> set_8051_sfr code_memory s sfr v
3570 | SFR_TH1 -> set_8051_sfr code_memory s sfr v
3572 let status_1 = set_8051_sfr code_memory s SFR_P1 v in
3573 set_p1_latch code_memory s v
3574 | SFR_SCON -> set_8051_sfr code_memory s sfr v
3575 | SFR_SBUF -> set_8051_sfr code_memory s sfr v
3576 | SFR_IE -> set_8051_sfr code_memory s sfr v
3578 let status_1 = set_8051_sfr code_memory s SFR_P3 v in
3579 set_p3_latch code_memory s v
3580 | SFR_IP -> set_8051_sfr code_memory s sfr v
3581 | SFR_PSW -> set_8051_sfr code_memory s sfr v
3582 | SFR_ACC_A -> set_8051_sfr code_memory s sfr v
3583 | SFR_ACC_B -> set_8051_sfr code_memory s sfr v)
3584 | Types.Inr sfr -> set_8052_sfr code_memory s sfr v)
3586 (** val bit_address_of_register :
3587 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.bitVector **)
3588 let bit_address_of_register code_memory s r =
3589 let b = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r Nat.O in
3590 let c = Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r (Nat.S Nat.O) in
3592 Vector.get_index_v (Nat.S (Nat.S (Nat.S Nat.O))) r (Nat.S (Nat.S Nat.O))
3594 let r1 = get_rs1_flag code_memory s in
3595 let r0 = get_rs0_flag code_memory s in
3597 match Bool.andb (Bool.notb r1) (Bool.notb r0) with
3598 | Bool.True -> Nat.O
3600 (match Bool.andb (Bool.notb r1) r0 with
3602 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
3604 (match Bool.andb r1 r0 with
3606 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3607 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3608 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3609 Nat.O)))))))))))))))))))))))
3611 Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3612 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3613 Nat.O)))))))))))))))))
3615 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3618 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
3619 (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
3620 (Vector.VCons ((Nat.S (Nat.S Nat.O)), b, (Vector.VCons ((Nat.S
3621 Nat.O), c, (Vector.VCons (Nat.O, d, Vector.VEmpty))))))))))
3623 (** val get_register :
3624 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte **)
3625 let get_register code_memory s r =
3626 let address = bit_address_of_register code_memory s r in
3627 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3628 Nat.O))))))) address s.low_internal_ram
3629 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3632 (** val set_register :
3633 'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
3635 let set_register code_memory s r v =
3636 let address = bit_address_of_register code_memory s r in
3637 update_low_internal_ram code_memory s address v
3639 (** val read_from_external_ram :
3640 'a1 -> 'a1 preStatus -> BitVector.word -> BitVector.byte **)
3641 let read_from_external_ram code_memory s addr =
3642 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3643 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3644 Nat.O)))))))))))))))) addr s.external_ram
3645 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3648 (** val read_from_internal_ram :
3649 'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte **)
3650 let read_from_internal_ram code_memory s addr =
3651 let { Types.fst = bit_one; Types.snd = seven_bits } =
3652 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3653 (Nat.S Nat.O))))))) addr
3656 match Vector.head' Nat.O bit_one with
3657 | Bool.True -> s.high_internal_ram
3658 | Bool.False -> s.low_internal_ram
3660 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3661 Nat.O))))))) seven_bits memory
3662 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3665 (** val read_at_stack_pointer : 'a1 -> 'a1 preStatus -> BitVector.byte **)
3666 let read_at_stack_pointer code_memory s =
3667 read_from_internal_ram code_memory s (get_8051_sfr code_memory s SFR_SP)
3669 (** val write_at_stack_pointer :
3670 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus **)
3671 let write_at_stack_pointer code_memory s v =
3672 let { Types.fst = bit_one; Types.snd = seven_bits } =
3673 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3674 (Nat.S Nat.O))))))) (get_8051_sfr code_memory s SFR_SP)
3676 (match Vector.head' Nat.O bit_one with
3677 | Bool.True -> update_high_internal_ram code_memory s seven_bits v
3678 | Bool.False -> update_low_internal_ram code_memory s seven_bits v)
3680 (** val set_arg_16' :
3681 'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
3682 preStatus Types.sig0 **)
3683 let set_arg_16' code_memory s v a =
3684 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Dptr,
3685 Vector.VEmpty)) a with
3686 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
3687 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3688 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3689 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
3690 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
3691 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3694 (let { Types.fst = bu; Types.snd = bl } =
3695 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3696 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3697 (Nat.S (Nat.S Nat.O)))))))) v
3700 let status0 = set_8051_sfr code_memory s SFR_DPH bu in
3701 let status1 = set_8051_sfr code_memory status0 SFR_DPL bl in status1))
3703 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3704 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3705 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3706 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3707 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3708 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3709 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3710 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3711 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3712 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3713 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3714 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3716 (** val set_arg_16 :
3717 'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
3719 let set_arg_16 code_memory s h h1 =
3720 Types.pi1 (set_arg_16' code_memory s h h1)
3722 (** val get_arg_16 :
3723 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word **)
3724 let get_arg_16 cm s a =
3725 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
3726 ASM.Data16, (Vector.VCons (Nat.O, ASM.Acc_dptr, Vector.VEmpty))))
3728 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
3729 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3730 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3731 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
3732 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
3733 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3734 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3735 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3736 | ASM.DATA16 d -> (fun _ -> d)
3740 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3741 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3742 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3743 (get_8051_sfr cm s SFR_DPL)
3746 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3747 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3748 (Nat.S (Nat.S Nat.O))))))))
3749 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3750 (Nat.S Nat.O))))))))) (get_8051_sfr cm s SFR_ACC_A)
3753 (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3754 Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3755 (Nat.S Nat.O))))))))) big_acc dptr)
3756 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3757 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3758 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3759 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3760 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3761 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3762 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3763 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3764 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3767 'a1 -> 'a1 preStatus -> Bool.bool -> ASM.subaddressing_mode ->
3769 let get_arg_8 cm s l a =
3770 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3771 (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons ((Nat.S (Nat.S
3772 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))),
3773 ASM.Direct, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3774 (Nat.S (Nat.S (Nat.S Nat.O)))))))), ASM.Indirect, (Vector.VCons
3775 ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
3776 ASM.Registr, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3777 (Nat.S Nat.O)))))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S
3778 (Nat.S (Nat.S Nat.O))))), ASM.Acc_b, (Vector.VCons ((Nat.S (Nat.S
3779 (Nat.S (Nat.S Nat.O)))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S
3780 (Nat.S Nat.O))), ASM.Acc_dptr, (Vector.VCons ((Nat.S (Nat.S
3781 Nat.O)), ASM.Acc_pc, (Vector.VCons ((Nat.S Nat.O),
3782 ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
3783 Vector.VEmpty)))))))))))))))))))) a with
3786 let { Types.fst = hd; Types.snd = seven_bits } =
3787 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3788 (Nat.S (Nat.S Nat.O))))))) d
3790 (match Vector.head' Nat.O hd with
3792 get_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S
3793 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, seven_bits))
3796 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3797 (Nat.S Nat.O))))))) seven_bits s.low_internal_ram
3798 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3799 (Nat.S Nat.O)))))))))))
3802 let { Types.fst = hd; Types.snd = seven_bits } =
3803 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3804 (Nat.S (Nat.S Nat.O)))))))
3805 (get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)),
3806 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
3807 (Vector.VCons (Nat.O, i, Vector.VEmpty)))))))
3809 (match Vector.head' Nat.O hd with
3811 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3812 (Nat.S Nat.O))))))) seven_bits s.high_internal_ram
3813 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3814 (Nat.S Nat.O)))))))))
3816 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3817 (Nat.S Nat.O))))))) seven_bits s.low_internal_ram
3818 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3819 (Nat.S Nat.O)))))))))))
3820 | ASM.EXT_INDIRECT e ->
3823 get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
3824 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
3827 let padded_address =
3828 BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3829 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3830 (Nat.S (Nat.S Nat.O)))))))) address
3832 read_from_external_ram cm s padded_address)
3833 | ASM.REGISTER r -> (fun _ -> get_register cm s r)
3834 | ASM.ACC_A -> (fun _ -> get_8051_sfr cm s SFR_ACC_A)
3835 | ASM.ACC_B -> (fun _ -> get_8051_sfr cm s SFR_ACC_B)
3836 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3837 | ASM.DATA d -> (fun _ -> d)
3838 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3842 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3843 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3844 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3845 (get_8051_sfr cm s SFR_DPL)
3848 BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3849 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3850 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_ACC_A)
3852 let { Types.fst = carry; Types.snd = address } =
3853 Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3854 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3855 Nat.O)))))))))))))))) dptr padded_acc
3857 read_from_external_ram cm s address)
3861 BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3862 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3863 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_ACC_A)
3865 let { Types.fst = carry; Types.snd = address } =
3866 Arithmetic.half_add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3867 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3868 Nat.O)))))))))))))))) s.program_counter padded_acc
3870 read_from_external_ram cm s address)
3871 | ASM.EXT_INDIRECT_DPTR ->
3874 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3875 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3876 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3877 (get_8051_sfr cm s SFR_DPL)
3879 read_from_external_ram cm s address)
3880 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3881 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3882 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3883 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3884 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3885 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3886 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3889 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.byte -> 'a1
3891 let set_arg_8 cm s a v =
3892 (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3893 Nat.O)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3894 (Nat.S Nat.O)))))), ASM.Direct, (Vector.VCons ((Nat.S (Nat.S
3895 (Nat.S (Nat.S (Nat.S Nat.O))))), ASM.Indirect, (Vector.VCons
3896 ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Registr, (Vector.VCons
3897 ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
3898 (Nat.S Nat.O)), ASM.Acc_b, (Vector.VCons ((Nat.S Nat.O),
3899 ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr,
3900 Vector.VEmpty)))))))))))))) a with
3903 let { Types.fst = bit_one; Types.snd = seven_bits } =
3904 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3905 (Nat.S (Nat.S Nat.O))))))) d
3907 (match Vector.head' Nat.O bit_one with
3909 set_bit_addressable_sfr cm s (Vector.VCons ((Nat.S (Nat.S (Nat.S
3910 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, seven_bits))
3912 | Bool.False -> update_low_internal_ram cm s seven_bits v))
3916 get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
3917 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, i,
3920 let { Types.fst = bit_one; Types.snd = seven_bits } =
3921 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3922 (Nat.S (Nat.S Nat.O))))))) register
3924 (match Vector.head' Nat.O bit_one with
3925 | Bool.True -> update_high_internal_ram cm s seven_bits v
3926 | Bool.False -> update_low_internal_ram cm s seven_bits v))
3927 | ASM.EXT_INDIRECT e ->
3930 get_register cm s (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
3931 (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, e,
3934 let padded_address =
3935 BitVector.pad (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3936 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3937 (Nat.S (Nat.S Nat.O)))))))) address
3939 update_external_ram cm s padded_address v)
3940 | ASM.REGISTER r -> (fun _ -> set_register cm s r v)
3941 | ASM.ACC_A -> (fun _ -> set_8051_sfr cm s SFR_ACC_A v)
3942 | ASM.ACC_B -> (fun _ -> set_8051_sfr cm s SFR_ACC_B v)
3943 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3944 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3945 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3946 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3947 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3948 | ASM.EXT_INDIRECT_DPTR ->
3951 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3952 (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3953 (Nat.S (Nat.S Nat.O)))))))) (get_8051_sfr cm s SFR_DPH)
3954 (get_8051_sfr cm s SFR_DPL)
3956 update_external_ram cm s address v)
3957 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3958 | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3959 | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3960 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3961 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3962 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3963 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
3966 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> Bool.bool -> Bool.bool **)
3967 let get_arg_1 cm s a l =
3968 (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
3969 (Nat.S Nat.O)), ASM.Bit_addr, (Vector.VCons ((Nat.S Nat.O),
3970 ASM.N_bit_addr, (Vector.VCons (Nat.O, ASM.Carry,
3971 Vector.VEmpty)))))) a with
3972 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
3973 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3974 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3975 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
3976 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
3977 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3978 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3979 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3980 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3981 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3982 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3983 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3984 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3985 | ASM.CARRY -> (fun _ -> get_cy_flag cm s)
3988 let { Types.fst = bit_1; Types.snd = seven_bits } =
3989 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3990 (Nat.S (Nat.S Nat.O))))))) b
3992 let { Types.fst = four_bits; Types.snd = three_bits } =
3993 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
3994 (Nat.S Nat.O))) seven_bits
3996 (match Vector.head' Nat.O bit_1 with
3999 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
4000 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
4001 (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
4002 ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
4003 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
4006 let sfr = get_bit_addressable_sfr cm s trans l in
4007 Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4008 (Nat.S Nat.O)))))))) sfr
4009 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4013 Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4014 (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
4015 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
4016 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
4019 BitVectorTrie.lookup
4020 (Nat.plus (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4021 (Nat.S Nat.O))))) address' s.low_internal_ram
4022 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4023 (Nat.S (Nat.S Nat.O)))))))))
4025 Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4026 (Nat.S Nat.O)))))))) t
4027 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4029 | ASM.N_BIT_ADDR n ->
4031 let { Types.fst = bit_1; Types.snd = seven_bits } =
4032 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4033 (Nat.S (Nat.S Nat.O))))))) n
4035 let { Types.fst = four_bits; Types.snd = three_bits } =
4036 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
4037 (Nat.S Nat.O))) seven_bits
4039 (match Vector.head' Nat.O bit_1 with
4042 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
4043 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
4044 (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
4045 ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
4046 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
4049 let sfr = get_bit_addressable_sfr cm s trans l in
4051 (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4052 (Nat.S (Nat.S Nat.O)))))))) sfr
4053 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4057 Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4058 (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
4059 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
4060 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
4063 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4064 (Nat.S Nat.O))))))) address' s.low_internal_ram
4065 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4066 (Nat.S (Nat.S Nat.O)))))))))
4069 (Vector.get_index_v (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4070 (Nat.S (Nat.S Nat.O)))))))) t
4071 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4073 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
4074 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
4075 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
4078 'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.bit -> 'a1
4080 let set_arg_1 cm s a v =
4081 (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
4082 ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.Carry, Vector.VEmpty)))) a with
4083 | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
4084 | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
4085 | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
4086 | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
4087 | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
4088 | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
4089 | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
4090 | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
4091 | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
4092 | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
4093 | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
4094 | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
4095 | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
4098 let { Types.fst = ignore; Types.snd = seven_bits } =
4099 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4100 (Nat.S (Nat.S Nat.O))))))) (get_8051_sfr cm s SFR_PSW)
4102 let new_psw = Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4103 (Nat.S Nat.O))))))), v, seven_bits)
4105 set_8051_sfr cm s SFR_PSW new_psw)
4108 let { Types.fst = bit_1; Types.snd = seven_bits } =
4109 Vector.vsplit (Nat.S Nat.O) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4110 (Nat.S (Nat.S Nat.O))))))) b
4112 let { Types.fst = four_bits; Types.snd = three_bits } =
4113 Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Nat.S (Nat.S
4114 (Nat.S Nat.O))) seven_bits
4116 (match Vector.head' Nat.O bit_1 with
4119 Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
4120 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
4121 (Nat.S (Nat.S Nat.O)))), Bool.True, four_bits)) (Vector.VCons
4122 ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S
4123 Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
4126 let sfr = get_bit_addressable_sfr cm s trans Bool.True in
4128 Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4129 (Nat.S Nat.O)))))))) sfr
4130 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4133 set_bit_addressable_sfr cm s new_sfr trans
4136 Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
4137 (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S Nat.O)),
4138 Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
4139 (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) four_bits
4142 BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4143 (Nat.S Nat.O))))))) address' s.low_internal_ram
4144 (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4145 (Nat.S (Nat.S Nat.O)))))))))
4148 Vector.set_index (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4149 (Nat.S Nat.O)))))))) t
4150 (Arithmetic.nat_of_bitvector (Nat.S (Nat.S (Nat.S Nat.O)))
4153 update_low_internal_ram cm s address' n_bit))
4154 | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
4155 | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
4156 | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
4157 | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
4159 (** val construct_datalabels :
4160 (ASM.identifier, BitVector.word) Types.prod List.list -> BitVector.word
4161 Identifiers.identifier_map **)
4162 let construct_datalabels the_preamble =
4163 (Util.foldl (fun t preamble ->
4164 let { Types.fst = datalabels; Types.snd = addr } = t in
4165 let { Types.fst = name; Types.snd = size } = preamble in
4166 let { Types.fst = addr0; Types.snd = carry } =
4167 Arithmetic.sub_16_with_carry addr size Bool.False
4170 (Identifiers.add PreIdentifiers.ASMTag datalabels name addr0);
4171 Types.snd = addr0 }) { Types.fst =
4172 (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
4173 (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4174 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
4175 Nat.O))))))))))))))))) } the_preamble).Types.fst