source: driver/extracted/csem.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: 13.7 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open Division
16
17open Z
18
19open BitVectorZ
20
21open Pointers
22
23open GenMem
24
25open FrontEndMem
26
27open Proper
28
29open PositiveMap
30
31open Deqsets
32
33open Extralib
34
35open Lists
36
37open Identifiers
38
39open Exp
40
41open Arithmetic
42
43open Vector
44
45open Div_and_mod
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Extranat
54
55open Integers
56
57open AST
58
59open ErrorMessages
60
61open Option
62
63open Setoids
64
65open Monad
66
67open Jmeq
68
69open Russell
70
71open Positive
72
73open PreIdentifiers
74
75open Bool
76
77open Relations
78
79open Nat
80
81open List
82
83open Hints_declaration
84
85open Core_notation
86
87open Pts
88
89open Logic
90
91open Types
92
93open Errors
94
95open Globalenvs
96
97open CostLabel
98
99open Csyntax
100
101open Events
102
103open Smallstep
104
105open TypeComparison
106
107open ClassifyOp
108
109val sem_neg : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
110
111val sem_notint : Values.val0 -> Values.val0 Types.option
112
113val sem_notbool : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
114
115val sem_add :
116  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
117  Types.option
118
119val sem_sub :
120  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
121  Csyntax.type0 -> Values.val0 Types.option
122
123val sem_mul :
124  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
125  Types.option
126
127val sem_div :
128  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
129  Types.option
130
131val sem_mod :
132  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
133  Types.option
134
135val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
136
137val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
138
139val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
140
141val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
142
143val sem_shr :
144  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
145  Types.option
146
147val sem_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
148
149val sem_cmp_match : Integers.comparison -> Values.val0 Types.option
150
151val sem_cmp :
152  Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
153  Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option
154
155val cast_bool_to_target :
156  Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option
157
158val sem_unary_operation :
159  Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
160  Types.option
161
162val sem_binary_operation :
163  Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
164  Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0 Types.option
165
166val cast_int_int :
167  AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
168  BitVector.bitVector
169
170type genv = Csyntax.clight_fundef Globalenvs.genv_t
171
172type env = Pointers.block Identifiers.identifier_map
173
174val empty_env : env
175
176val load_value_of_type :
177  Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
178  Values.val0 Types.option
179
180val store_value_of_type :
181  Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
182  Values.val0 -> GenMem.mem Types.option
183
184val blocks_of_env : env -> Pointers.block List.list
185
186val select_switch :
187  AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
188  Csyntax.labeled_statements Types.option
189
190val seq_of_labeled_statement :
191  Csyntax.labeled_statements -> Csyntax.statement
192
193type cont =
194| Kstop
195| Kseq of Csyntax.statement * cont
196| Kwhile of Csyntax.expr * Csyntax.statement * cont
197| Kdowhile of Csyntax.expr * Csyntax.statement * cont
198| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
199| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
200| Kswitch of cont
201| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
202           Types.prod Types.option * Csyntax.function0 * env * cont
203
204val cont_rect_Type4 :
205  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
206  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
207  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
208  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
209  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
210  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
211  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
212  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
213
214val cont_rect_Type3 :
215  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
216  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
217  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
218  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
219  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
220  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
221  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
222  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
223
224val cont_rect_Type2 :
225  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
226  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
227  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
228  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
229  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
230  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
231  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
232  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
233
234val cont_rect_Type1 :
235  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
236  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
237  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
238  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
239  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
240  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
241  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
242  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
243
244val cont_rect_Type0 :
245  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
246  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
247  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
248  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
249  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
250  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
251  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
252  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
253
254val cont_inv_rect_Type4 :
255  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
256  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
257  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
258  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
259  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
260  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
261  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
262  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
263  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
264
265val cont_inv_rect_Type3 :
266  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
267  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
268  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
269  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
270  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
271  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
272  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
273  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
274  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
275
276val cont_inv_rect_Type2 :
277  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
278  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
279  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
280  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
281  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
282  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
283  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
284  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
285  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
286
287val cont_inv_rect_Type1 :
288  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
289  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
290  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
291  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
292  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
293  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
294  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
295  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
296  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
297
298val cont_inv_rect_Type0 :
299  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
300  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
301  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
302  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
303  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
304  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
305  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
306  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
307  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
308
309val cont_discr : cont -> cont -> __
310
311val cont_jmdiscr : cont -> cont -> __
312
313val call_cont : cont -> cont
314
315type state =
316| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
317| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
318   * cont * GenMem.mem
319| Returnstate of Values.val0 * cont * GenMem.mem
320| Finalstate of Integers.int
321
322val state_rect_Type4 :
323  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
324  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
325  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
326  (Integers.int -> 'a1) -> state -> 'a1
327
328val state_rect_Type5 :
329  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
330  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
331  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
332  (Integers.int -> 'a1) -> state -> 'a1
333
334val state_rect_Type3 :
335  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
336  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
337  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
338  (Integers.int -> 'a1) -> state -> 'a1
339
340val state_rect_Type2 :
341  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
342  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
343  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
344  (Integers.int -> 'a1) -> state -> 'a1
345
346val state_rect_Type1 :
347  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
348  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
349  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
350  (Integers.int -> 'a1) -> state -> 'a1
351
352val state_rect_Type0 :
353  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
354  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
355  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
356  (Integers.int -> 'a1) -> state -> 'a1
357
358val state_inv_rect_Type4 :
359  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
360  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
361  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
362  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
363
364val state_inv_rect_Type3 :
365  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
366  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
367  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
368  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
369
370val state_inv_rect_Type2 :
371  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
372  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
373  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
374  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
375
376val state_inv_rect_Type1 :
377  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
378  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
379  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
380  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
381
382val state_inv_rect_Type0 :
383  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
384  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
385  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
386  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
387
388val state_discr : state -> state -> __
389
390val state_jmdiscr : state -> state -> __
391
392val find_label_ls :
393  Csyntax.label -> Csyntax.labeled_statements -> cont -> (Csyntax.statement,
394  cont) Types.prod Types.option
395
396val find_label :
397  Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
398  Types.prod Types.option
399
400val fun_typeof : Csyntax.expr -> Csyntax.type0
401
Note: See TracBrowser for help on using the repository browser.