source: extracted/rTLabs_syntax.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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