source: extracted/rTLabs_syntax.mli @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 8 years ago

...

File size: 18.1 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Proper
12
13open PositiveMap
14
15open Deqsets
16
17open ErrorMessages
18
19open PreIdentifiers
20
21open Errors
22
23open Extralib
24
25open Setoids
26
27open Monad
28
29open Option
30
31open Lists
32
33open Positive
34
35open Identifiers
36
37open Arithmetic
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Types
66
67open AST
68
69open CostLabel
70
71open FrontEndVal
72
73open Hide
74
75open ByteValues
76
77open GenMem
78
79open FrontEndMem
80
81open Division
82
83open Z
84
85open BitVectorZ
86
87open Pointers
88
89open Coqlib
90
91open Values
92
93open FrontEndOps
94
95open Order
96
97open Registers
98
99open BitVectorTrie
100
101open Graphs
102
103type statement =
104| St_skip of Graphs.label
105| St_cost of CostLabel.costlabel * Graphs.label
106| St_const of AST.typ * Registers.register * FrontEndOps.constant
107   * Graphs.label
108| St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
109   * Registers.register * Registers.register * Graphs.label
110| St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
111   * Registers.register * Registers.register * Registers.register
112   * Graphs.label
113| St_load of AST.typ * Registers.register * Registers.register * Graphs.label
114| St_store of AST.typ * Registers.register * Registers.register
115   * Graphs.label
116| St_call_id of AST.ident * Registers.register List.list
117   * Registers.register Types.option * Graphs.label
118| St_call_ptr of Registers.register * Registers.register List.list
119   * Registers.register Types.option * Graphs.label
120| St_cond of Registers.register * Graphs.label * Graphs.label
121| St_return
122
123val statement_rect_Type4 :
124  (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
125  (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
126  'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
127  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
128  (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
129  Registers.register -> Registers.register -> Registers.register ->
130  Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
131  Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
132  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
133  (AST.ident -> Registers.register List.list -> Registers.register
134  Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
135  Registers.register List.list -> Registers.register Types.option ->
136  Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
137  -> 'a1) -> 'a1 -> statement -> 'a1
138
139val statement_rect_Type5 :
140  (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
141  (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
142  'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
143  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
144  (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
145  Registers.register -> Registers.register -> Registers.register ->
146  Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
147  Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
148  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
149  (AST.ident -> Registers.register List.list -> Registers.register
150  Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
151  Registers.register List.list -> Registers.register Types.option ->
152  Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
153  -> 'a1) -> 'a1 -> statement -> 'a1
154
155val statement_rect_Type3 :
156  (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
157  (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
158  'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
159  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
160  (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
161  Registers.register -> Registers.register -> Registers.register ->
162  Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
163  Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
164  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
165  (AST.ident -> Registers.register List.list -> Registers.register
166  Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
167  Registers.register List.list -> Registers.register Types.option ->
168  Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
169  -> 'a1) -> 'a1 -> statement -> 'a1
170
171val statement_rect_Type2 :
172  (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
173  (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
174  'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
175  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
176  (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
177  Registers.register -> Registers.register -> Registers.register ->
178  Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
179  Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
180  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
181  (AST.ident -> Registers.register List.list -> Registers.register
182  Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
183  Registers.register List.list -> Registers.register Types.option ->
184  Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
185  -> 'a1) -> 'a1 -> statement -> 'a1
186
187val statement_rect_Type1 :
188  (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
189  (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
190  'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
191  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
192  (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
193  Registers.register -> Registers.register -> Registers.register ->
194  Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
195  Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
196  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
197  (AST.ident -> Registers.register List.list -> Registers.register
198  Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
199  Registers.register List.list -> Registers.register Types.option ->
200  Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
201  -> 'a1) -> 'a1 -> statement -> 'a1
202
203val statement_rect_Type0 :
204  (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
205  (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
206  'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
207  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
208  (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
209  Registers.register -> Registers.register -> Registers.register ->
210  Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
211  Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
212  Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
213  (AST.ident -> Registers.register List.list -> Registers.register
214  Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
215  Registers.register List.list -> Registers.register Types.option ->
216  Graphs.label -> 'a1) -> (Registers.register -> Graphs.label -> Graphs.label
217  -> 'a1) -> 'a1 -> statement -> 'a1
218
219val statement_inv_rect_Type4 :
220  statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
221  Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
222  FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
223  -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
224  -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
225  FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
226  Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
227  Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
228  (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
229  -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
230  Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
231  Registers.register List.list -> Registers.register Types.option ->
232  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
233  Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
234
235val statement_inv_rect_Type3 :
236  statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
237  Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
238  FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
239  -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
240  -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
241  FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
242  Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
243  Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
244  (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
245  -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
246  Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
247  Registers.register List.list -> Registers.register Types.option ->
248  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
249  Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
250
251val statement_inv_rect_Type2 :
252  statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
253  Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
254  FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
255  -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
256  -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
257  FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
258  Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
259  Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
260  (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
261  -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
262  Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
263  Registers.register List.list -> Registers.register Types.option ->
264  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
265  Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
266
267val statement_inv_rect_Type1 :
268  statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
269  Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
270  FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
271  -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
272  -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
273  FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
274  Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
275  Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
276  (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
277  -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
278  Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
279  Registers.register List.list -> Registers.register Types.option ->
280  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
281  Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
282
283val statement_inv_rect_Type0 :
284  statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
285  Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
286  FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
287  -> FrontEndOps.unary_operation -> Registers.register -> Registers.register
288  -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ -> AST.typ ->
289  FrontEndOps.binary_operation -> Registers.register -> Registers.register ->
290  Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ ->
291  Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
292  (AST.typ -> Registers.register -> Registers.register -> Graphs.label -> __
293  -> 'a1) -> (AST.ident -> Registers.register List.list -> Registers.register
294  Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
295  Registers.register List.list -> Registers.register Types.option ->
296  Graphs.label -> __ -> 'a1) -> (Registers.register -> Graphs.label ->
297  Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1
298
299val statement_jmdiscr : statement -> statement -> __
300
301type internal_function = { f_labgen : Identifiers.universe;
302                           f_reggen : Identifiers.universe;
303                           f_result : (Registers.register, AST.typ)
304                                      Types.prod Types.option;
305                           f_params : (Registers.register, AST.typ)
306                                      Types.prod List.list;
307                           f_locals : (Registers.register, AST.typ)
308                                      Types.prod List.list;
309                           f_stacksize : Nat.nat;
310                           f_graph : statement Graphs.graph;
311                           f_entry : Graphs.label Types.sig0;
312                           f_exit : Graphs.label Types.sig0 }
313
314val internal_function_rect_Type4 :
315  (Identifiers.universe -> Identifiers.universe -> (Registers.register,
316  AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
317  Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
318  -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
319  -> Graphs.label Types.sig0 -> 'a1) -> internal_function -> 'a1
320
321val internal_function_rect_Type5 :
322  (Identifiers.universe -> Identifiers.universe -> (Registers.register,
323  AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
324  Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
325  -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
326  -> Graphs.label Types.sig0 -> 'a1) -> internal_function -> 'a1
327
328val internal_function_rect_Type3 :
329  (Identifiers.universe -> Identifiers.universe -> (Registers.register,
330  AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
331  Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
332  -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
333  -> Graphs.label Types.sig0 -> 'a1) -> internal_function -> 'a1
334
335val internal_function_rect_Type2 :
336  (Identifiers.universe -> Identifiers.universe -> (Registers.register,
337  AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
338  Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
339  -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
340  -> Graphs.label Types.sig0 -> 'a1) -> internal_function -> 'a1
341
342val internal_function_rect_Type1 :
343  (Identifiers.universe -> Identifiers.universe -> (Registers.register,
344  AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
345  Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
346  -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
347  -> Graphs.label Types.sig0 -> 'a1) -> internal_function -> 'a1
348
349val internal_function_rect_Type0 :
350  (Identifiers.universe -> Identifiers.universe -> (Registers.register,
351  AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
352  Types.prod List.list -> (Registers.register, AST.typ) Types.prod List.list
353  -> Nat.nat -> statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0
354  -> Graphs.label Types.sig0 -> 'a1) -> internal_function -> 'a1
355
356val f_labgen : internal_function -> Identifiers.universe
357
358val f_reggen : internal_function -> Identifiers.universe
359
360val f_result :
361  internal_function -> (Registers.register, AST.typ) Types.prod Types.option
362
363val f_params :
364  internal_function -> (Registers.register, AST.typ) Types.prod List.list
365
366val f_locals :
367  internal_function -> (Registers.register, AST.typ) Types.prod List.list
368
369val f_stacksize : internal_function -> Nat.nat
370
371val f_graph : internal_function -> statement Graphs.graph
372
373val f_entry : internal_function -> Graphs.label Types.sig0
374
375val f_exit : internal_function -> Graphs.label Types.sig0
376
377val internal_function_inv_rect_Type4 :
378  internal_function -> (Identifiers.universe -> Identifiers.universe ->
379  (Registers.register, AST.typ) Types.prod Types.option ->
380  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
381  AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
382  __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
383  'a1
384
385val internal_function_inv_rect_Type3 :
386  internal_function -> (Identifiers.universe -> Identifiers.universe ->
387  (Registers.register, AST.typ) Types.prod Types.option ->
388  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
389  AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
390  __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
391  'a1
392
393val internal_function_inv_rect_Type2 :
394  internal_function -> (Identifiers.universe -> Identifiers.universe ->
395  (Registers.register, AST.typ) Types.prod Types.option ->
396  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
397  AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
398  __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
399  'a1
400
401val internal_function_inv_rect_Type1 :
402  internal_function -> (Identifiers.universe -> Identifiers.universe ->
403  (Registers.register, AST.typ) Types.prod Types.option ->
404  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
405  AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
406  __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
407  'a1
408
409val internal_function_inv_rect_Type0 :
410  internal_function -> (Identifiers.universe -> Identifiers.universe ->
411  (Registers.register, AST.typ) Types.prod Types.option ->
412  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
413  AST.typ) Types.prod List.list -> Nat.nat -> statement Graphs.graph -> __ ->
414  __ -> Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
415  'a1
416
417val internal_function_jmdiscr : internal_function -> internal_function -> __
418
419type rTLabs_program = (internal_function AST.fundef, Nat.nat) AST.program
420
Note: See TracBrowser for help on using the repository browser.