source: extracted/status.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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