source: driver/extracted/frontEndOps.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 23.4 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Integers
16
17open AST
18
19open Division
20
21open Exp
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open FrontEndVal
84
85open Hide
86
87open ByteValues
88
89open GenMem
90
91open FrontEndMem
92
93type constant =
94| Ointconst of AST.intsize * AST.signedness * AST.bvint
95| Oaddrsymbol of AST.ident * Nat.nat
96| Oaddrstack of Nat.nat
97
98val constant_rect_Type4 :
99  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
100  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
101
102val constant_rect_Type5 :
103  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
104  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
105
106val constant_rect_Type3 :
107  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
108  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
109
110val constant_rect_Type2 :
111  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
112  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
113
114val constant_rect_Type1 :
115  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
116  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
117
118val constant_rect_Type0 :
119  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
120  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
121
122val constant_inv_rect_Type4 :
123  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
124  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
125  -> __ -> 'a1) -> 'a1
126
127val constant_inv_rect_Type3 :
128  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
129  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
130  -> __ -> 'a1) -> 'a1
131
132val constant_inv_rect_Type2 :
133  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
134  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
135  -> __ -> 'a1) -> 'a1
136
137val constant_inv_rect_Type1 :
138  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
139  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
140  -> __ -> 'a1) -> 'a1
141
142val constant_inv_rect_Type0 :
143  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
144  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
145  -> __ -> 'a1) -> 'a1
146
147val constant_discr : AST.typ -> constant -> constant -> __
148
149val constant_jmdiscr : AST.typ -> constant -> constant -> __
150
151type unary_operation =
152| Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
153| Onegint of AST.intsize * AST.signedness
154| Onotbool of AST.typ * AST.intsize * AST.signedness
155| Onotint of AST.intsize * AST.signedness
156| Oid of AST.typ
157| Optrofint of AST.intsize * AST.signedness
158| Ointofptr of AST.intsize * AST.signedness
159
160val unary_operation_rect_Type4 :
161  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
162  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
163  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
164  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
165  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
166
167val unary_operation_rect_Type5 :
168  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
169  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
170  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
171  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
172  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
173
174val unary_operation_rect_Type3 :
175  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
176  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
177  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
178  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
179  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
180
181val unary_operation_rect_Type2 :
182  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
183  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
184  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
185  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
186  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
187
188val unary_operation_rect_Type1 :
189  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
190  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
191  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
192  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
193  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
194
195val unary_operation_rect_Type0 :
196  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
197  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
198  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
199  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
200  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
201
202val unary_operation_inv_rect_Type4 :
203  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
204  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
205  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
206  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
207  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
208  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
209  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
210
211val unary_operation_inv_rect_Type3 :
212  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
213  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
214  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
215  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
216  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
217  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
218  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
219
220val unary_operation_inv_rect_Type2 :
221  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
222  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
223  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
224  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
225  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
226  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
227  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
228
229val unary_operation_inv_rect_Type1 :
230  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
231  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
232  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
233  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
234  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
235  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
236  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
237
238val unary_operation_inv_rect_Type0 :
239  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
240  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
241  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
242  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
243  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
244  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
245  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
246
247val unary_operation_discr :
248  AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
249
250val unary_operation_jmdiscr :
251  AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
252
253type binary_operation =
254| Oadd of AST.intsize * AST.signedness
255| Osub of AST.intsize * AST.signedness
256| Omul of AST.intsize * AST.signedness
257| Odiv of AST.intsize
258| Odivu of AST.intsize
259| Omod of AST.intsize
260| Omodu of AST.intsize
261| Oand of AST.intsize * AST.signedness
262| Oor of AST.intsize * AST.signedness
263| Oxor of AST.intsize * AST.signedness
264| Oshl of AST.intsize * AST.signedness
265| Oshr of AST.intsize * AST.signedness
266| Oshru of AST.intsize * AST.signedness
267| Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
268| Ocmpu of AST.intsize * AST.signedness * Integers.comparison
269| Oaddpi of AST.intsize
270| Oaddip of AST.intsize
271| Osubpi of AST.intsize
272| Osubpp of AST.intsize
273| Ocmpp of AST.signedness * Integers.comparison
274
275val binary_operation_rect_Type4 :
276  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
277  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
278  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
279  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
280  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
281  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
282  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
283  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
284  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
285  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
286  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
287  AST.typ -> binary_operation -> 'a1
288
289val binary_operation_rect_Type5 :
290  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
291  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
292  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
293  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
294  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
295  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
296  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
297  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
298  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
299  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
300  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
301  AST.typ -> binary_operation -> 'a1
302
303val binary_operation_rect_Type3 :
304  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
305  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
306  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
307  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
308  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
309  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
310  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
311  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
312  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
313  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
314  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
315  AST.typ -> binary_operation -> 'a1
316
317val binary_operation_rect_Type2 :
318  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
319  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
320  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
321  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
322  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
323  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
324  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
325  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
326  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
327  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
328  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
329  AST.typ -> binary_operation -> 'a1
330
331val binary_operation_rect_Type1 :
332  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
333  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
334  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
335  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
336  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
337  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
338  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
339  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
340  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
341  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
342  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
343  AST.typ -> binary_operation -> 'a1
344
345val binary_operation_rect_Type0 :
346  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
347  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
348  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
349  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
350  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
351  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
352  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
353  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
354  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
355  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
356  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
357  AST.typ -> binary_operation -> 'a1
358
359val binary_operation_inv_rect_Type4 :
360  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
361  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
362  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
363  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
364  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
365  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
366  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
367  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
368  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
369  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
370  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
371  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
372  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
373  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
374  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
375  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
376  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
377  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
378  -> __ -> __ -> 'a1) -> 'a1
379
380val binary_operation_inv_rect_Type3 :
381  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
382  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
383  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
384  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
385  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
386  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
387  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
388  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
389  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
390  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
391  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
392  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
393  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
394  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
395  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
396  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
397  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
398  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
399  -> __ -> __ -> 'a1) -> 'a1
400
401val binary_operation_inv_rect_Type2 :
402  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
403  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
404  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
405  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
406  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
407  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
408  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
409  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
410  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
411  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
412  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
413  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
414  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
415  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
416  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
417  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
418  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
419  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
420  -> __ -> __ -> 'a1) -> 'a1
421
422val binary_operation_inv_rect_Type1 :
423  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
424  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
425  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
426  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
427  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
428  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
429  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
430  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
431  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
432  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
433  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
434  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
435  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
436  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
437  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
438  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
439  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
440  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
441  -> __ -> __ -> 'a1) -> 'a1
442
443val binary_operation_inv_rect_Type0 :
444  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
445  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
446  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
447  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
448  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
449  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
450  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
451  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
452  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
453  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
454  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
455  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
456  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
457  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
458  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
459  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
460  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
461  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
462  -> __ -> __ -> 'a1) -> 'a1
463
464val binary_operation_discr :
465  AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
466
467val binary_operation_jmdiscr :
468  AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
469
470val eval_constant :
471  AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block ->
472  constant -> Values.val0 Types.option
473
474val eval_unop :
475  AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
476  Types.option
477
478val eval_compare_mismatch : Integers.comparison -> Values.val0 Types.option
479
480val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option
481
482val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option
483
484val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
485
486val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
487
488val ev_subpp :
489  AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option
490
491val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option
492
493val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option
494
495val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option
496
497val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option
498
499val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option
500
501val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
502
503val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
504
505val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
506
507val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
508
509val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option
510
511val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option
512
513val fEtrue : Values.val0
514
515val fEfalse : Values.val0
516
517val fE_of_bool : Bool.bool -> Values.val0
518
519val ev_cmp_match : Integers.comparison -> Values.val0 Types.option
520
521val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
522
523val ev_cmp :
524  Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
525  Types.option
526
527val ev_cmpp :
528  GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
529  Values.val0 Types.option
530
531val ev_cmpu :
532  Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
533  Types.option
534
535val eval_binop :
536  GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
537  Values.val0 -> Values.val0 -> Values.val0 Types.option
538
Note: See TracBrowser for help on using the repository browser.