source: extracted/rTLabs_syntax.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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