source: extracted/status.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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