source: extracted/backEndOps.mli @ 2933

Last change on this file since 2933 was 2933, checked in by sacerdot, 6 years ago

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File size: 8.6 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 Lists
20
21open Identifiers
22
23open Integers
24
25open AST
26
27open Division
28
29open Exp
30
31open Arithmetic
32
33open Setoids
34
35open Monad
36
37open Option
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
83val divmodZ : Z.z -> Z.z -> (Z.z, Z.z) Types.prod
84
85type opAccs =
86| Mul
87| DivuModu
88
89val opAccs_rect_Type4 : 'a1 -> 'a1 -> opAccs -> 'a1
90
91val opAccs_rect_Type5 : 'a1 -> 'a1 -> opAccs -> 'a1
92
93val opAccs_rect_Type3 : 'a1 -> 'a1 -> opAccs -> 'a1
94
95val opAccs_rect_Type2 : 'a1 -> 'a1 -> opAccs -> 'a1
96
97val opAccs_rect_Type1 : 'a1 -> 'a1 -> opAccs -> 'a1
98
99val opAccs_rect_Type0 : 'a1 -> 'a1 -> opAccs -> 'a1
100
101val opAccs_inv_rect_Type4 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
102
103val opAccs_inv_rect_Type3 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
104
105val opAccs_inv_rect_Type2 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
106
107val opAccs_inv_rect_Type1 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
108
109val opAccs_inv_rect_Type0 : opAccs -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
110
111val opAccs_discr : opAccs -> opAccs -> __
112
113val opAccs_jmdiscr : opAccs -> opAccs -> __
114
115type op1 =
116| Cmpl
117| Inc
118| Rl
119
120val op1_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
121
122val op1_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
123
124val op1_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
125
126val op1_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
127
128val op1_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
129
130val op1_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> op1 -> 'a1
131
132val op1_inv_rect_Type4 :
133  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
134
135val op1_inv_rect_Type3 :
136  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
137
138val op1_inv_rect_Type2 :
139  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
140
141val op1_inv_rect_Type1 :
142  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
143
144val op1_inv_rect_Type0 :
145  op1 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
146
147val op1_discr : op1 -> op1 -> __
148
149val op1_jmdiscr : op1 -> op1 -> __
150
151type op2 =
152| Add
153| Addc
154| Sub
155| And
156| Or
157| Xor
158
159val op2_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
160
161val op2_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
162
163val op2_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
164
165val op2_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
166
167val op2_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
168
169val op2_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> op2 -> 'a1
170
171val op2_inv_rect_Type4 :
172  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
173  'a1) -> (__ -> 'a1) -> 'a1
174
175val op2_inv_rect_Type3 :
176  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
177  'a1) -> (__ -> 'a1) -> 'a1
178
179val op2_inv_rect_Type2 :
180  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
181  'a1) -> (__ -> 'a1) -> 'a1
182
183val op2_inv_rect_Type1 :
184  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
185  'a1) -> (__ -> 'a1) -> 'a1
186
187val op2_inv_rect_Type0 :
188  op2 -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
189  'a1) -> (__ -> 'a1) -> 'a1
190
191val op2_discr : op2 -> op2 -> __
192
193val op2_jmdiscr : op2 -> op2 -> __
194
195type eval = { opaccs : (opAccs -> BitVector.byte -> BitVector.byte ->
196                       (BitVector.byte, BitVector.byte) Types.prod);
197              op0 : (op1 -> BitVector.byte -> BitVector.byte);
198              op3 : (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte
199                    -> (BitVector.byte, BitVector.bit) Types.prod) }
200
201val eval_rect_Type4 :
202  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
203  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
204  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
205  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
206
207val eval_rect_Type5 :
208  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
209  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
210  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
211  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
212
213val eval_rect_Type3 :
214  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
215  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
216  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
217  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
218
219val eval_rect_Type2 :
220  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
221  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
222  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
223  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
224
225val eval_rect_Type1 :
226  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
227  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
228  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
229  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
230
231val eval_rect_Type0 :
232  ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
233  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
234  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
235  (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1
236
237val opaccs :
238  eval -> opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
239  BitVector.byte) Types.prod
240
241val op0 : eval -> op1 -> BitVector.byte -> BitVector.byte
242
243val op3 :
244  eval -> BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
245  (BitVector.byte, BitVector.bit) Types.prod
246
247val eval_inv_rect_Type4 :
248  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
249  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
250  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
251  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
252
253val eval_inv_rect_Type3 :
254  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
255  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
256  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
257  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
258
259val eval_inv_rect_Type2 :
260  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
261  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
262  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
263  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
264
265val eval_inv_rect_Type1 :
266  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
267  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
268  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
269  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
270
271val eval_inv_rect_Type0 :
272  eval -> ((opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
273  BitVector.byte) Types.prod) -> (op1 -> BitVector.byte -> BitVector.byte) ->
274  (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
275  (BitVector.byte, BitVector.bit) Types.prod) -> __ -> 'a1) -> 'a1
276
277val eval_discr : eval -> eval -> __
278
279val eval_jmdiscr : eval -> eval -> __
280
281val opaccs_implementation :
282  opAccs -> BitVector.byte -> BitVector.byte -> (BitVector.byte,
283  BitVector.byte) Types.prod
284
285val op1_implementation : op1 -> BitVector.byte -> BitVector.byte
286
287val op2_implementation :
288  BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
289  (BitVector.byte, BitVector.bit) Types.prod
290
291val eval0 : eval
292
293val be_opaccs :
294  opAccs -> ByteValues.beval -> ByteValues.beval -> (ByteValues.beval,
295  ByteValues.beval) Types.prod Errors.res
296
297val be_op1 : op1 -> ByteValues.beval -> ByteValues.beval Errors.res
298
299val op2_bytes :
300  op2 -> Nat.nat -> BitVector.bit -> BitVector.byte Vector.vector ->
301  BitVector.byte Vector.vector -> (BitVector.byte Vector.vector,
302  BitVector.bit) Types.prod
303
304val op_of_add_or_sub : ByteValues.add_or_sub -> op2
305
306val be_add_sub_byte :
307  ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
308  BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
309  Errors.res
310
311val byte_at : Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte
312
313val eq_opt :
314  ('a1 -> 'a1 -> Bool.bool) -> 'a1 Types.option -> 'a1 Types.option ->
315  Bool.bool
316
317val be_op2 :
318  ByteValues.bebit -> op2 -> ByteValues.beval -> ByteValues.beval ->
319  (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res
320
Note: See TracBrowser for help on using the repository browser.