source: extracted/i8051.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: 6.5 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Jmeq
18
19open Exp
20
21open Extranat
22
23open Vector
24
25open Div_and_mod
26
27open Russell
28
29open Types
30
31open List
32
33open Util
34
35open FoldStuff
36
37open BitVector
38
39open Arithmetic
40
41val int_size : BitVector.bitVector
42
43val ptr_size : BitVector.bitVector
44
45val alignment : 'a1 Types.option
46
47type register =
48| Register00
49| Register01
50| Register02
51| Register03
52| Register04
53| Register05
54| Register06
55| Register07
56| Register10
57| Register11
58| Register12
59| Register13
60| Register14
61| Register15
62| Register16
63| Register17
64| Register20
65| Register21
66| Register22
67| Register23
68| Register24
69| Register25
70| Register26
71| Register27
72| Register30
73| Register31
74| Register32
75| Register33
76| Register34
77| Register35
78| Register36
79| Register37
80| RegisterA
81| RegisterB
82| RegisterDPL
83| RegisterDPH
84| RegisterCarry
85
86val register_rect_Type4 :
87  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
88  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
89  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
90  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
91
92val register_rect_Type5 :
93  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
94  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
95  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
96  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
97
98val register_rect_Type3 :
99  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
100  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
101  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
102  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
103
104val register_rect_Type2 :
105  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
106  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
107  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
108  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
109
110val register_rect_Type1 :
111  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
112  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
113  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
114  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
115
116val register_rect_Type0 :
117  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
118  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 ->
119  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
120  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
121
122val register_inv_rect_Type4 :
123  register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
124  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
125  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
126  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
127  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
128  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
129  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
130  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
131
132val register_inv_rect_Type3 :
133  register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
134  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
135  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
136  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
137  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
138  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
139  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
140  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
141
142val register_inv_rect_Type2 :
143  register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
144  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
145  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
146  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
147  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
148  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
149  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
150  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
151
152val register_inv_rect_Type1 :
153  register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
154  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
155  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
156  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
157  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
158  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
159  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
160  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
161
162val register_inv_rect_Type0 :
163  register -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
164  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
165  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
166  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
167  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
168  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
169  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
170  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
171
172val register_discr : register -> register -> __
173
174val register_jmdiscr : register -> register -> __
175
176val nat_of_register : register -> Nat.nat
177
178val physical_register_count : Nat.nat
179
180val bitvector_of_register : register -> BitVector.bitVector
181
182val eq_Register : register -> register -> Bool.bool
183
184val registerSST : register
185
186val registerST0 : register
187
188val registerST1 : register
189
190val registerST2 : register
191
192val registerST3 : register
193
194val registerSTS : register List.list
195
196val registerSPL : register
197
198val registerSPH : register
199
200val registerParams : register List.list
201
202val registers : register List.list
203
204val registerRets : register List.list
205
206val registerCallerSaved : register List.list
207
208val registerCalleeSaved : register List.list
209
210val registersForbidden : register List.list
211
212val registersAllocatable : register List.list
213
Note: See TracBrowser for help on using the repository browser.