source: extracted/status.mli @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 17.0 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open Arithmetic
8
9open Integers
10
11open AST
12
13open CostLabel
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open ErrorMessages
22
23open PreIdentifiers
24
25open Errors
26
27open Extralib
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Lists
36
37open Positive
38
39open Identifiers
40
41open Extranat
42
43open Vector
44
45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Types
52
53open List
54
55open Util
56
57open FoldStuff
58
59open Bool
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Relations
70
71open Nat
72
73open BitVector
74
75open ASM
76
77open BitVectorTrie
78
79type time = Nat.nat
80
81type serialBufferType =
82| Eight of BitVector.byte
83| Nine of BitVector.bit * BitVector.byte
84
85val serialBufferType_rect_Type4 :
86  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
87  serialBufferType -> 'a1
88
89val serialBufferType_rect_Type5 :
90  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
91  serialBufferType -> 'a1
92
93val serialBufferType_rect_Type3 :
94  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
95  serialBufferType -> 'a1
96
97val serialBufferType_rect_Type2 :
98  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
99  serialBufferType -> 'a1
100
101val serialBufferType_rect_Type1 :
102  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
103  serialBufferType -> 'a1
104
105val serialBufferType_rect_Type0 :
106  (BitVector.byte -> 'a1) -> (BitVector.bit -> BitVector.byte -> 'a1) ->
107  serialBufferType -> 'a1
108
109val serialBufferType_inv_rect_Type4 :
110  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
111  BitVector.byte -> __ -> 'a1) -> 'a1
112
113val serialBufferType_inv_rect_Type3 :
114  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
115  BitVector.byte -> __ -> 'a1) -> 'a1
116
117val serialBufferType_inv_rect_Type2 :
118  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
119  BitVector.byte -> __ -> 'a1) -> 'a1
120
121val serialBufferType_inv_rect_Type1 :
122  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
123  BitVector.byte -> __ -> 'a1) -> 'a1
124
125val serialBufferType_inv_rect_Type0 :
126  serialBufferType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit ->
127  BitVector.byte -> __ -> 'a1) -> 'a1
128
129val serialBufferType_discr : serialBufferType -> serialBufferType -> __
130
131val serialBufferType_jmdiscr : serialBufferType -> serialBufferType -> __
132
133type lineType =
134| P2 of BitVector.byte
135| P3 of BitVector.byte
136| SerialBuffer of serialBufferType
137
138val lineType_rect_Type4 :
139  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
140  'a1) -> lineType -> 'a1
141
142val lineType_rect_Type5 :
143  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
144  'a1) -> lineType -> 'a1
145
146val lineType_rect_Type3 :
147  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
148  'a1) -> lineType -> 'a1
149
150val lineType_rect_Type2 :
151  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
152  'a1) -> lineType -> 'a1
153
154val lineType_rect_Type1 :
155  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
156  'a1) -> lineType -> 'a1
157
158val lineType_rect_Type0 :
159  (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> (serialBufferType ->
160  'a1) -> lineType -> 'a1
161
162val lineType_inv_rect_Type4 :
163  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
164  -> (serialBufferType -> __ -> 'a1) -> 'a1
165
166val lineType_inv_rect_Type3 :
167  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
168  -> (serialBufferType -> __ -> 'a1) -> 'a1
169
170val lineType_inv_rect_Type2 :
171  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
172  -> (serialBufferType -> __ -> 'a1) -> 'a1
173
174val lineType_inv_rect_Type1 :
175  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
176  -> (serialBufferType -> __ -> 'a1) -> 'a1
177
178val lineType_inv_rect_Type0 :
179  lineType -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1)
180  -> (serialBufferType -> __ -> 'a1) -> 'a1
181
182val lineType_discr : lineType -> lineType -> __
183
184val lineType_jmdiscr : lineType -> lineType -> __
185
186type sFR8051 =
187| SFR_SP
188| SFR_DPL
189| SFR_DPH
190| SFR_PCON
191| SFR_TCON
192| SFR_TMOD
193| SFR_TL0
194| SFR_TL1
195| SFR_TH0
196| SFR_TH1
197| SFR_P1
198| SFR_SCON
199| SFR_SBUF
200| SFR_IE
201| SFR_P3
202| SFR_IP
203| SFR_PSW
204| SFR_ACC_A
205| SFR_ACC_B
206
207val sFR8051_rect_Type4 :
208  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
209  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
210
211val sFR8051_rect_Type5 :
212  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
213  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
214
215val sFR8051_rect_Type3 :
216  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
217  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
218
219val sFR8051_rect_Type2 :
220  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
221  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
222
223val sFR8051_rect_Type1 :
224  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
225  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
226
227val sFR8051_rect_Type0 :
228  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
229  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8051 -> 'a1
230
231val sFR8051_inv_rect_Type4 :
232  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
233  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
234  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
235  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
236
237val sFR8051_inv_rect_Type3 :
238  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
239  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
240  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
241  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
242
243val sFR8051_inv_rect_Type2 :
244  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
245  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
246  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
247  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
248
249val sFR8051_inv_rect_Type1 :
250  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
251  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
252  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
253  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
254
255val sFR8051_inv_rect_Type0 :
256  sFR8051 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
257  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
258  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
259  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
260
261val sFR8051_discr : sFR8051 -> sFR8051 -> __
262
263val sFR8051_jmdiscr : sFR8051 -> sFR8051 -> __
264
265val sfr_8051_index : sFR8051 -> Nat.nat
266
267type sFR8052 =
268| SFR_T2CON
269| SFR_RCAP2L
270| SFR_RCAP2H
271| SFR_TL2
272| SFR_TH2
273
274val sFR8052_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
275
276val sFR8052_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
277
278val sFR8052_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
279
280val sFR8052_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
281
282val sFR8052_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
283
284val sFR8052_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> sFR8052 -> 'a1
285
286val sFR8052_inv_rect_Type4 :
287  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
288  -> 'a1) -> 'a1
289
290val sFR8052_inv_rect_Type3 :
291  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
292  -> 'a1) -> 'a1
293
294val sFR8052_inv_rect_Type2 :
295  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
296  -> 'a1) -> 'a1
297
298val sFR8052_inv_rect_Type1 :
299  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
300  -> 'a1) -> 'a1
301
302val sFR8052_inv_rect_Type0 :
303  sFR8052 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
304  -> 'a1) -> 'a1
305
306val sFR8052_discr : sFR8052 -> sFR8052 -> __
307
308val sFR8052_jmdiscr : sFR8052 -> sFR8052 -> __
309
310val sfr_8052_index : sFR8052 -> Nat.nat
311
312type 'm preStatus = { low_internal_ram : BitVector.byte
313                                         BitVectorTrie.bitVectorTrie;
314                      high_internal_ram : BitVector.byte
315                                          BitVectorTrie.bitVectorTrie;
316                      external_ram : BitVector.byte
317                                     BitVectorTrie.bitVectorTrie;
318                      program_counter : BitVector.word;
319                      special_function_registers_8051 : BitVector.byte
320                                                        Vector.vector;
321                      special_function_registers_8052 : BitVector.byte
322                                                        Vector.vector;
323                      p1_latch : BitVector.byte; p3_latch : BitVector.byte;
324                      clock : time }
325
326val preStatus_rect_Type4 :
327  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
328  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
329  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
330  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
331  preStatus -> 'a2
332
333val preStatus_rect_Type5 :
334  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
335  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
336  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
337  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
338  preStatus -> 'a2
339
340val preStatus_rect_Type3 :
341  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
342  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
343  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
344  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
345  preStatus -> 'a2
346
347val preStatus_rect_Type2 :
348  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
349  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
350  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
351  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
352  preStatus -> 'a2
353
354val preStatus_rect_Type1 :
355  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
356  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
357  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
358  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
359  preStatus -> 'a2
360
361val preStatus_rect_Type0 :
362  'a1 -> (BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
363  BitVectorTrie.bitVectorTrie -> BitVector.byte BitVectorTrie.bitVectorTrie
364  -> BitVector.word -> BitVector.byte Vector.vector -> BitVector.byte
365  Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
366  preStatus -> 'a2
367
368val low_internal_ram :
369  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
370
371val high_internal_ram :
372  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
373
374val external_ram :
375  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie
376
377val program_counter : 'a1 -> 'a1 preStatus -> BitVector.word
378
379val special_function_registers_8051 :
380  'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector
381
382val special_function_registers_8052 :
383  'a1 -> 'a1 preStatus -> BitVector.byte Vector.vector
384
385val p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte
386
387val p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte
388
389val clock : 'a1 -> 'a1 preStatus -> time
390
391val preStatus_inv_rect_Type4 :
392  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
393  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
394  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
395  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
396  BitVector.byte -> time -> __ -> 'a2) -> 'a2
397
398val preStatus_inv_rect_Type3 :
399  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
400  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
401  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
402  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
403  BitVector.byte -> time -> __ -> 'a2) -> 'a2
404
405val preStatus_inv_rect_Type2 :
406  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
407  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
408  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
409  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
410  BitVector.byte -> time -> __ -> 'a2) -> 'a2
411
412val preStatus_inv_rect_Type1 :
413  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
414  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
415  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
416  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
417  BitVector.byte -> time -> __ -> 'a2) -> 'a2
418
419val preStatus_inv_rect_Type0 :
420  'a1 -> 'a1 preStatus -> (BitVector.byte BitVectorTrie.bitVectorTrie ->
421  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.byte
422  BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte
423  Vector.vector -> BitVector.byte Vector.vector -> BitVector.byte ->
424  BitVector.byte -> time -> __ -> 'a2) -> 'a2
425
426val preStatus_jmdiscr : 'a1 -> 'a1 preStatus -> 'a1 preStatus -> __
427
428type status = BitVector.byte BitVectorTrie.bitVectorTrie preStatus
429
430type pseudoStatus = ASM.pseudo_assembly_program preStatus
431
432val set_clock : 'a1 -> 'a1 preStatus -> time -> 'a1 preStatus
433
434val set_p1_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
435
436val set_p3_latch : 'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
437
438val get_8051_sfr : 'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte
439
440val get_8052_sfr : 'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte
441
442val set_8051_sfr :
443  'a1 -> 'a1 preStatus -> sFR8051 -> BitVector.byte -> 'a1 preStatus
444
445val set_8052_sfr :
446  'a1 -> 'a1 preStatus -> sFR8052 -> BitVector.byte -> 'a1 preStatus
447
448val set_program_counter :
449  'a1 -> 'a1 preStatus -> BitVector.word -> 'a1 preStatus
450
451val set_code_memory : 'a1 -> 'a1 preStatus -> 'a2 -> 'a2 preStatus
452
453val set_low_internal_ram :
454  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
455  preStatus
456
457val set_high_internal_ram :
458  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
459  preStatus
460
461val set_external_ram :
462  'a1 -> 'a1 preStatus -> BitVector.byte BitVectorTrie.bitVectorTrie -> 'a1
463  preStatus
464
465val get_cy_flag : 'a1 -> 'a1 preStatus -> Bool.bool
466
467val get_ac_flag : 'a1 -> 'a1 preStatus -> Bool.bool
468
469val get_fo_flag : 'a1 -> 'a1 preStatus -> Bool.bool
470
471val get_rs1_flag : 'a1 -> 'a1 preStatus -> Bool.bool
472
473val get_rs0_flag : 'a1 -> 'a1 preStatus -> Bool.bool
474
475val get_ov_flag : 'a1 -> 'a1 preStatus -> Bool.bool
476
477val get_ud_flag : 'a1 -> 'a1 preStatus -> Bool.bool
478
479val get_p_flag : 'a1 -> 'a1 preStatus -> Bool.bool
480
481val set_flags :
482  'a1 -> 'a1 preStatus -> BitVector.bit -> BitVector.bit Types.option ->
483  BitVector.bit -> 'a1 preStatus
484
485val initialise_status : 'a1 -> 'a1 preStatus
486
487val sfr_of_Byte : BitVector.byte -> (sFR8051, sFR8052) Types.sum Types.option
488
489val get_bit_addressable_sfr :
490  'a1 -> 'a1 preStatus -> BitVector.byte -> Bool.bool -> BitVector.byte
491
492val set_bit_addressable_sfr :
493  'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte -> 'a1 preStatus
494
495val bit_address_of_register :
496  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.bitVector
497
498val get_register :
499  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte
500
501val set_register :
502  'a1 -> 'a1 preStatus -> BitVector.bitVector -> BitVector.byte -> 'a1
503  preStatus
504
505val read_from_internal_ram :
506  'a1 -> 'a1 preStatus -> BitVector.byte -> BitVector.byte
507
508val read_at_stack_pointer : 'a1 -> 'a1 preStatus -> BitVector.byte
509
510val write_at_stack_pointer :
511  'a1 -> 'a1 preStatus -> BitVector.byte -> 'a1 preStatus
512
513val set_arg_16' :
514  'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
515  preStatus Types.sig0
516
517val set_arg_16 :
518  'a1 -> 'a1 preStatus -> BitVector.word -> ASM.subaddressing_mode -> 'a1
519  preStatus
520
521val get_arg_16 :
522  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.word
523
524val get_arg_8 :
525  'a1 -> 'a1 preStatus -> Bool.bool -> ASM.subaddressing_mode ->
526  BitVector.byte
527
528val set_arg_8 :
529  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.byte -> 'a1
530  preStatus
531
532val get_arg_1 :
533  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> Bool.bool -> Bool.bool
534
535val set_arg_1 :
536  'a1 -> 'a1 preStatus -> ASM.subaddressing_mode -> BitVector.bit -> 'a1
537  preStatus
538
539val fetch_pseudo_instruction :
540  ASM.labelled_instruction List.list -> BitVector.word ->
541  (ASM.pseudo_instruction, BitVector.word) Types.prod
542
543val construct_datalabels :
544  ASM.preamble -> BitVector.word Identifiers.identifier_map
545
Note: See TracBrowser for help on using the repository browser.