source: extracted/backEndOps.mli @ 2717

Last change on this file since 2717 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: 8.5 KB
Line 
1open Preamble
2
3open Hide
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Identifiers
28
29open Integers
30
31open AST
32
33open Division
34
35open Exp
36
37open Arithmetic
38
39open Extranat
40
41open Vector
42
43open Div_and_mod
44
45open Jmeq
46
47open Russell
48
49open List
50
51open Util
52
53open FoldStuff
54
55open BitVector
56
57open Types
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Positive
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open ByteValues
82
83type opAccs =
84| Mul
85| DivuModu
86
87val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1
88
89val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1
90
91val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1
92
93val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1
94
95val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1
96
97val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1
98
99val opAccs_inv_rect_Type4 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
100
101val opAccs_inv_rect_Type3 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
102
103val opAccs_inv_rect_Type2 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
104
105val opAccs_inv_rect_Type1 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
106
107val opAccs_inv_rect_Type0 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
108
109val opAccs_discr : opAccs -> opAccs -> __
110
111val opAccs_jmdiscr : opAccs -> opAccs -> __
112
113type op1 =
114| Cmpl
115| Inc
116| Rl
117
118val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
119
120val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
121
122val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
123
124val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
125
126val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
127
128val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
129
130val op1_inv_rect_Type4 :
131  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
132
133val op1_inv_rect_Type3 :
134  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
135
136val op1_inv_rect_Type2 :
137  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
138
139val op1_inv_rect_Type1 :
140  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
141
142val op1_inv_rect_Type0 :
143  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
144
145val op1_discr : op1 -> op1 -> __
146
147val op1_jmdiscr : op1 -> op1 -> __
148
149type op2 =
150| Add
151| Addc
152| Sub
153| And
154| Or
155| Xor
156
157val op2_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
158
159val op2_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
160
161val op2_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
162
163val op2_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
164
165val op2_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
166
167val op2_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
168
169val op2_inv_rect_Type4 :
170  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
171  'a1) -> (__ -> 'a1) -> 'a1
172
173val op2_inv_rect_Type3 :
174  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
175  'a1) -> (__ -> 'a1) -> 'a1
176
177val op2_inv_rect_Type2 :
178  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
179  'a1) -> (__ -> 'a1) -> 'a1
180
181val op2_inv_rect_Type1 :
182  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
183  'a1) -> (__ -> 'a1) -> 'a1
184
185val op2_inv_rect_Type0 :
186  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
187  'a1) -> (__ -> 'a1) -> 'a1
188
189val op2_discr : op2 -> op2 -> __
190
191val op2_jmdiscr : op2 -> op2 -> __
192
193type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
194                       (BitVector.byte, BitVector.byte) Types.prod);
195              op0 : (op1 -> BitVector.byte -> BitVector.byte);
196              op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
197                    -> (BitVector.byte, BitVector.bit) Types.prod) }
198
199val eval_rect_Type4 :
200  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
201  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
202  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
203  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
204
205val eval_rect_Type5 :
206  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
207  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
208  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
209  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
210
211val eval_rect_Type3 :
212  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
213  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
214  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
215  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
216
217val eval_rect_Type2 :
218  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
219  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
220  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
221  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
222
223val eval_rect_Type1 :
224  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
225  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
226  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
227  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
228
229val eval_rect_Type0 :
230  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
231  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
232  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
233  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
234
235val opaccs :
236  eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
237  BitVector.byte) Types.prod
238
239val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte
240
241val op3 :
242  eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
243  (BitVector.byte, BitVector.bit) Types.prod
244
245val eval_inv_rect_Type4 :
246  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
247  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
248  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
249  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
250
251val eval_inv_rect_Type3 :
252  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
253  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
254  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
255  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
256
257val eval_inv_rect_Type2 :
258  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
259  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
260  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
261  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
262
263val eval_inv_rect_Type1 :
264  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
265  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
266  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
267  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
268
269val eval_inv_rect_Type0 :
270  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
271  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
272  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
273  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
274
275val eval_discr : eval -> eval -> __
276
277val eval_jmdiscr : eval -> eval -> __
278
279val opaccs_implementation :
280  opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
281  BitVector.byte) Types.prod
282
283val op1_implementation : op1 -> BitVector.byte -> BitVector.byte
284
285val op2_implementation :
286  BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
287  (BitVector.byte, BitVector.bit) Types.prod
288
289val eval0 : eval
290
291val be_opaccs :
292  opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
293  ByteValues.beval) Types.prod Errors.res
294
295val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res
296
297val op2_bytes :
298  op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
299  BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
300  BitVector.bit) Types.prod
301
302val be_add_sub_byte :
303  Bool.bool -> ByteValues.bebit -> ByteValues.beval -> BitVector.byte ->
304  (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res
305
306val byte_at : Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte
307
308val eq_opt :
309  ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
310  Bool.bool
311
312val be_op2 :
313  ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
314  (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res
315
Note: See TracBrowser for help on using the repository browser.