source: extracted/joint.mli @ 2717

Last change on this file since 2717 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: 33.6 KB
Line 
1open Preamble
2
3open Hide
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Identifiers
28
29open Integers
30
31open AST
32
33open Division
34
35open Exp
36
37open Arithmetic
38
39open Extranat
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 Types
58
59open Bool
60
61open Relations
62
63open Nat
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Positive
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open ByteValues
82
83open BackEndOps
84
85open BitVectorTrie
86
87open CostLabel
88
89open Order
90
91open Registers
92
93open I8051
94
95open Graphs
96
97open LabelledObjects
98
99open Sets
100
101open Listb
102
103open String
104
105type 't argument =
106| Reg of 't
107| Imm of BitVector.byte
108
109val argument_rect_Type4 :
110  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
111
112val argument_rect_Type5 :
113  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
114
115val argument_rect_Type3 :
116  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
117
118val argument_rect_Type2 :
119  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
120
121val argument_rect_Type1 :
122  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
123
124val argument_rect_Type0 :
125  ('a1 -> 'a2) -> (BitVector.byte -> 'a2) -> 'a1 argument -> 'a2
126
127val argument_inv_rect_Type4 :
128  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
129
130val argument_inv_rect_Type3 :
131  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
132
133val argument_inv_rect_Type2 :
134  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
135
136val argument_inv_rect_Type1 :
137  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
138
139val argument_inv_rect_Type0 :
140  'a1 argument -> ('a1 -> __ -> 'a2) -> (BitVector.byte -> __ -> 'a2) -> 'a2
141
142val argument_discr : 'a1 argument -> 'a1 argument -> __
143
144val argument_jmdiscr : 'a1 argument -> 'a1 argument -> __
145
146type psd_argument = Registers.register argument
147
148val psd_argument_from_reg : Registers.register -> psd_argument
149
150val psd_argument_from_byte : BitVector.byte -> psd_argument
151
152type hdw_argument = I8051.register argument
153
154val hdw_argument_from_reg : I8051.register -> hdw_argument
155
156val hdw_argument_from_byte : BitVector.byte -> hdw_argument
157
158val byte_of_nat : Nat.nat -> BitVector.byte
159
160val zero_byte : BitVector.byte
161
162type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
163                             has_tailcalls : Bool.bool }
164
165val unserialized_params_rect_Type4 :
166  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
167  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
168  unserialized_params -> 'a1
169
170val unserialized_params_rect_Type5 :
171  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
172  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
173  unserialized_params -> 'a1
174
175val unserialized_params_rect_Type3 :
176  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
177  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
178  unserialized_params -> 'a1
179
180val unserialized_params_rect_Type2 :
181  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
182  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
183  unserialized_params -> 'a1
184
185val unserialized_params_rect_Type1 :
186  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
187  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
188  unserialized_params -> 'a1
189
190val unserialized_params_rect_Type0 :
191  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
192  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
193  unserialized_params -> 'a1
194
195type acc_a_reg
196
197type acc_b_reg
198
199type acc_a_arg
200
201type acc_b_arg
202
203type dpl_reg
204
205type dph_reg
206
207type dpl_arg
208
209type dph_arg
210
211type snd_arg
212
213type pair_move
214
215type call_args
216
217type call_dest
218
219type ext_seq
220
221val ext_seq_labels : unserialized_params -> __ -> Graphs.label List.list
222
223val has_tailcalls : unserialized_params -> Bool.bool
224
225type paramsT
226
227val unserialized_params_inv_rect_Type4 :
228  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
229  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
230  __ -> __ -> 'a1) -> 'a1
231
232val unserialized_params_inv_rect_Type3 :
233  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
234  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
235  __ -> __ -> 'a1) -> 'a1
236
237val unserialized_params_inv_rect_Type2 :
238  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
239  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
240  __ -> __ -> 'a1) -> 'a1
241
242val unserialized_params_inv_rect_Type1 :
243  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
244  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
245  __ -> __ -> 'a1) -> 'a1
246
247val unserialized_params_inv_rect_Type0 :
248  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
249  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
250  __ -> __ -> 'a1) -> 'a1
251
252val unserialized_params_jmdiscr :
253  unserialized_params -> unserialized_params -> __
254
255type joint_seq =
256| COMMENT of String.string
257| MOVE of __
258| POP of __
259| PUSH of __
260| ADDRESS of AST.ident * __ * __
261| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
262| OP1 of BackEndOps.op1 * __ * __
263| OP2 of BackEndOps.op2 * __ * __ * __
264| CLEAR_CARRY
265| SET_CARRY
266| LOAD of __ * __ * __
267| STORE of __ * __ * __
268| Extension_seq of __
269
270val joint_seq_rect_Type4 :
271  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
272  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
273  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
274  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
275  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
276  (__ -> 'a1) -> joint_seq -> 'a1
277
278val joint_seq_rect_Type5 :
279  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
280  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
281  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
282  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
283  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
284  (__ -> 'a1) -> joint_seq -> 'a1
285
286val joint_seq_rect_Type3 :
287  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
288  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
289  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
290  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
291  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
292  (__ -> 'a1) -> joint_seq -> 'a1
293
294val joint_seq_rect_Type2 :
295  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
296  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
297  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
298  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
299  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
300  (__ -> 'a1) -> joint_seq -> 'a1
301
302val joint_seq_rect_Type1 :
303  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
304  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
305  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
306  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
307  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
308  (__ -> 'a1) -> joint_seq -> 'a1
309
310val joint_seq_rect_Type0 :
311  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
312  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
313  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
314  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
315  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
316  (__ -> 'a1) -> joint_seq -> 'a1
317
318val joint_seq_inv_rect_Type4 :
319  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
320  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
321  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
322  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
323  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
324  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
325  'a1) -> (__ -> __ -> 'a1) -> 'a1
326
327val joint_seq_inv_rect_Type3 :
328  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
329  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
330  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
331  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
332  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
333  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
334  'a1) -> (__ -> __ -> 'a1) -> 'a1
335
336val joint_seq_inv_rect_Type2 :
337  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
338  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
339  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
340  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
341  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
342  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
343  'a1) -> (__ -> __ -> 'a1) -> 'a1
344
345val joint_seq_inv_rect_Type1 :
346  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
347  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
348  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
349  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
350  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
351  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
352  'a1) -> (__ -> __ -> 'a1) -> 'a1
353
354val joint_seq_inv_rect_Type0 :
355  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
356  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
357  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
358  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
359  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
360  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
361  'a1) -> (__ -> __ -> 'a1) -> 'a1
362
363val joint_seq_discr :
364  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
365
366val joint_seq_jmdiscr :
367  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
368
369val nOOP : unserialized_params -> AST.ident List.list -> joint_seq
370
371type joint_step =
372| COST_LABEL of CostLabel.costlabel
373| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
374| COND of __ * Graphs.label
375| Step_seq of joint_seq
376
377val joint_step_rect_Type4 :
378  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
379  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
380  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
381
382val joint_step_rect_Type5 :
383  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
384  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
385  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
386
387val joint_step_rect_Type3 :
388  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
389  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
390  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
391
392val joint_step_rect_Type2 :
393  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
394  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
395  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
396
397val joint_step_rect_Type1 :
398  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
399  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
400  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
401
402val joint_step_rect_Type0 :
403  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
404  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
405  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
406
407val joint_step_inv_rect_Type4 :
408  unserialized_params -> AST.ident List.list -> joint_step ->
409  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
410  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
411  (joint_seq -> __ -> 'a1) -> 'a1
412
413val joint_step_inv_rect_Type3 :
414  unserialized_params -> AST.ident List.list -> joint_step ->
415  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
416  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
417  (joint_seq -> __ -> 'a1) -> 'a1
418
419val joint_step_inv_rect_Type2 :
420  unserialized_params -> AST.ident List.list -> joint_step ->
421  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
422  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
423  (joint_seq -> __ -> 'a1) -> 'a1
424
425val joint_step_inv_rect_Type1 :
426  unserialized_params -> AST.ident List.list -> joint_step ->
427  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
428  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
429  (joint_seq -> __ -> 'a1) -> 'a1
430
431val joint_step_inv_rect_Type0 :
432  unserialized_params -> AST.ident List.list -> joint_step ->
433  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
434  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
435  (joint_seq -> __ -> 'a1) -> 'a1
436
437val joint_step_discr :
438  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
439  __
440
441val joint_step_jmdiscr :
442  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
443  __
444
445val step_labels :
446  unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
447  List.list
448
449type stmt_params = { uns_pars : unserialized_params;
450                     succ_label : (__ -> Graphs.label Types.option);
451                     has_fcond : Bool.bool }
452
453val stmt_params_rect_Type4 :
454  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
455  Bool.bool -> 'a1) -> stmt_params -> 'a1
456
457val stmt_params_rect_Type5 :
458  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
459  Bool.bool -> 'a1) -> stmt_params -> 'a1
460
461val stmt_params_rect_Type3 :
462  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
463  Bool.bool -> 'a1) -> stmt_params -> 'a1
464
465val stmt_params_rect_Type2 :
466  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
467  Bool.bool -> 'a1) -> stmt_params -> 'a1
468
469val stmt_params_rect_Type1 :
470  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
471  Bool.bool -> 'a1) -> stmt_params -> 'a1
472
473val stmt_params_rect_Type0 :
474  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
475  Bool.bool -> 'a1) -> stmt_params -> 'a1
476
477val uns_pars : stmt_params -> unserialized_params
478
479type succ0
480
481val succ_label : stmt_params -> __ -> Graphs.label Types.option
482
483val has_fcond : stmt_params -> Bool.bool
484
485val stmt_params_inv_rect_Type4 :
486  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
487  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
488
489val stmt_params_inv_rect_Type3 :
490  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
491  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
492
493val stmt_params_inv_rect_Type2 :
494  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
495  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
496
497val stmt_params_inv_rect_Type1 :
498  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
499  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
500
501val stmt_params_inv_rect_Type0 :
502  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
503  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
504
505val stmt_params_jmdiscr : stmt_params -> stmt_params -> __
506
507type joint_fin_step =
508| GOTO of Graphs.label
509| RETURN
510| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
511
512val joint_fin_step_rect_Type4 :
513  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
514  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
515
516val joint_fin_step_rect_Type5 :
517  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
518  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
519
520val joint_fin_step_rect_Type3 :
521  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
522  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
523
524val joint_fin_step_rect_Type2 :
525  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
526  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
527
528val joint_fin_step_rect_Type1 :
529  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
530  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
531
532val joint_fin_step_rect_Type0 :
533  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
534  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
535
536val joint_fin_step_inv_rect_Type4 :
537  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
538  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
539  'a1) -> 'a1
540
541val joint_fin_step_inv_rect_Type3 :
542  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
543  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
544  'a1) -> 'a1
545
546val joint_fin_step_inv_rect_Type2 :
547  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
548  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
549  'a1) -> 'a1
550
551val joint_fin_step_inv_rect_Type1 :
552  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
553  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
554  'a1) -> 'a1
555
556val joint_fin_step_inv_rect_Type0 :
557  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
558  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
559  'a1) -> 'a1
560
561val joint_fin_step_discr :
562  unserialized_params -> joint_fin_step -> joint_fin_step -> __
563
564val joint_fin_step_jmdiscr :
565  unserialized_params -> joint_fin_step -> joint_fin_step -> __
566
567val fin_step_labels :
568  unserialized_params -> joint_fin_step -> Graphs.label List.list
569
570type joint_statement =
571| Sequential of joint_step * __
572| Final of joint_fin_step
573| FCOND of __ * Graphs.label * Graphs.label
574
575val joint_statement_rect_Type4 :
576  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
577  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
578  'a1) -> joint_statement -> 'a1
579
580val joint_statement_rect_Type5 :
581  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
582  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
583  'a1) -> joint_statement -> 'a1
584
585val joint_statement_rect_Type3 :
586  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
587  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
588  'a1) -> joint_statement -> 'a1
589
590val joint_statement_rect_Type2 :
591  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
592  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
593  'a1) -> joint_statement -> 'a1
594
595val joint_statement_rect_Type1 :
596  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
597  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
598  'a1) -> joint_statement -> 'a1
599
600val joint_statement_rect_Type0 :
601  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
602  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
603  'a1) -> joint_statement -> 'a1
604
605val joint_statement_inv_rect_Type4 :
606  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
607  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
608  -> Graphs.label -> __ -> 'a1) -> 'a1
609
610val joint_statement_inv_rect_Type3 :
611  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
612  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
613  -> Graphs.label -> __ -> 'a1) -> 'a1
614
615val joint_statement_inv_rect_Type2 :
616  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
617  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
618  -> Graphs.label -> __ -> 'a1) -> 'a1
619
620val joint_statement_inv_rect_Type1 :
621  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
622  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
623  -> Graphs.label -> __ -> 'a1) -> 'a1
624
625val joint_statement_inv_rect_Type0 :
626  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
627  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
628  -> Graphs.label -> __ -> 'a1) -> 'a1
629
630val joint_statement_discr :
631  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
632  __
633
634val joint_statement_jmdiscr :
635  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
636  __
637
638type params = { stmt_pars : stmt_params;
639                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
640                          Types.option);
641                point_of_label : (AST.ident List.list -> __ -> Graphs.label
642                                 -> __ Types.option);
643                point_of_succ : (__ -> __ -> __) }
644
645val params_rect_Type4 :
646  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
647  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
648  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
649
650val params_rect_Type5 :
651  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
652  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
653  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
654
655val params_rect_Type3 :
656  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
657  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
658  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
659
660val params_rect_Type2 :
661  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
662  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
663  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
664
665val params_rect_Type1 :
666  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
667  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
668  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
669
670val params_rect_Type0 :
671  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
672  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
673  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
674
675val stmt_pars : params -> stmt_params
676
677type codeT
678
679type code_point
680
681val stmt_at :
682  params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option
683
684val point_of_label :
685  params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option
686
687val point_of_succ : params -> __ -> __ -> __
688
689val params_inv_rect_Type4 :
690  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
691  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
692  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
693
694val params_inv_rect_Type3 :
695  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
696  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
697  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
698
699val params_inv_rect_Type2 :
700  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
701  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
702  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
703
704val params_inv_rect_Type1 :
705  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
706  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
707  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
708
709val params_inv_rect_Type0 :
710  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
711  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
712  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
713
714val params_jmdiscr : params -> params -> __
715
716val stmt_pars__o__uns_pars : params -> unserialized_params
717
718val code_has_point : params -> AST.ident List.list -> __ -> __ -> Bool.bool
719
720val code_has_label :
721  params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool
722
723val stmt_explicit_labels :
724  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
725  List.list
726
727val stmt_implicit_label :
728  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
729  Types.option
730
731val stmt_labels :
732  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
733  List.list
734
735type lin_params =
736  unserialized_params
737  (* singleton inductive, whose constructor was mk_lin_params *)
738
739val lin_params_rect_Type4 : (unserialized_params -> 'a1) -> lin_params -> 'a1
740
741val lin_params_rect_Type5 : (unserialized_params -> 'a1) -> lin_params -> 'a1
742
743val lin_params_rect_Type3 : (unserialized_params -> 'a1) -> lin_params -> 'a1
744
745val lin_params_rect_Type2 : (unserialized_params -> 'a1) -> lin_params -> 'a1
746
747val lin_params_rect_Type1 : (unserialized_params -> 'a1) -> lin_params -> 'a1
748
749val lin_params_rect_Type0 : (unserialized_params -> 'a1) -> lin_params -> 'a1
750
751val l_u_pars : lin_params -> unserialized_params
752
753val lin_params_inv_rect_Type4 :
754  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
755
756val lin_params_inv_rect_Type3 :
757  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
758
759val lin_params_inv_rect_Type2 :
760  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
761
762val lin_params_inv_rect_Type1 :
763  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
764
765val lin_params_inv_rect_Type0 :
766  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
767
768val lin_params_jmdiscr : lin_params -> lin_params -> __
769
770val lin_params_to_params : lin_params -> params
771
772type graph_params =
773  unserialized_params
774  (* singleton inductive, whose constructor was mk_graph_params *)
775
776val graph_params_rect_Type4 :
777  (unserialized_params -> 'a1) -> graph_params -> 'a1
778
779val graph_params_rect_Type5 :
780  (unserialized_params -> 'a1) -> graph_params -> 'a1
781
782val graph_params_rect_Type3 :
783  (unserialized_params -> 'a1) -> graph_params -> 'a1
784
785val graph_params_rect_Type2 :
786  (unserialized_params -> 'a1) -> graph_params -> 'a1
787
788val graph_params_rect_Type1 :
789  (unserialized_params -> 'a1) -> graph_params -> 'a1
790
791val graph_params_rect_Type0 :
792  (unserialized_params -> 'a1) -> graph_params -> 'a1
793
794val g_u_pars : graph_params -> unserialized_params
795
796val graph_params_inv_rect_Type4 :
797  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
798
799val graph_params_inv_rect_Type3 :
800  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
801
802val graph_params_inv_rect_Type2 :
803  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
804
805val graph_params_inv_rect_Type1 :
806  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
807
808val graph_params_inv_rect_Type0 :
809  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
810
811val graph_params_jmdiscr : graph_params -> graph_params -> __
812
813val graph_params_to_params : graph_params -> params
814
815type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
816                                 joint_if_runiverse : Identifiers.universe;
817                                 joint_if_result : __; joint_if_params : 
818                                 __; joint_if_stacksize : Nat.nat;
819                                 joint_if_code : __;
820                                 joint_if_entry : __ Types.sig0 }
821
822val joint_internal_function_rect_Type4 :
823  params -> AST.ident List.list -> (Identifiers.universe ->
824  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
825  -> joint_internal_function -> 'a1
826
827val joint_internal_function_rect_Type5 :
828  params -> AST.ident List.list -> (Identifiers.universe ->
829  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
830  -> joint_internal_function -> 'a1
831
832val joint_internal_function_rect_Type3 :
833  params -> AST.ident List.list -> (Identifiers.universe ->
834  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
835  -> joint_internal_function -> 'a1
836
837val joint_internal_function_rect_Type2 :
838  params -> AST.ident List.list -> (Identifiers.universe ->
839  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
840  -> joint_internal_function -> 'a1
841
842val joint_internal_function_rect_Type1 :
843  params -> AST.ident List.list -> (Identifiers.universe ->
844  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
845  -> joint_internal_function -> 'a1
846
847val joint_internal_function_rect_Type0 :
848  params -> AST.ident List.list -> (Identifiers.universe ->
849  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
850  -> joint_internal_function -> 'a1
851
852val joint_if_luniverse :
853  params -> AST.ident List.list -> joint_internal_function ->
854  Identifiers.universe
855
856val joint_if_runiverse :
857  params -> AST.ident List.list -> joint_internal_function ->
858  Identifiers.universe
859
860val joint_if_result :
861  params -> AST.ident List.list -> joint_internal_function -> __
862
863val joint_if_params :
864  params -> AST.ident List.list -> joint_internal_function -> __
865
866val joint_if_stacksize :
867  params -> AST.ident List.list -> joint_internal_function -> Nat.nat
868
869val joint_if_code :
870  params -> AST.ident List.list -> joint_internal_function -> __
871
872val joint_if_entry :
873  params -> AST.ident List.list -> joint_internal_function -> __ Types.sig0
874
875val joint_internal_function_inv_rect_Type4 :
876  params -> AST.ident List.list -> joint_internal_function ->
877  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
878  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
879
880val joint_internal_function_inv_rect_Type3 :
881  params -> AST.ident List.list -> joint_internal_function ->
882  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
883  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
884
885val joint_internal_function_inv_rect_Type2 :
886  params -> AST.ident List.list -> joint_internal_function ->
887  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
888  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
889
890val joint_internal_function_inv_rect_Type1 :
891  params -> AST.ident List.list -> joint_internal_function ->
892  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
893  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
894
895val joint_internal_function_inv_rect_Type0 :
896  params -> AST.ident List.list -> joint_internal_function ->
897  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
898  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
899
900val joint_internal_function_jmdiscr :
901  params -> AST.ident List.list -> joint_internal_function ->
902  joint_internal_function -> __
903
904val good_if_rect_Type4 :
905  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
906  -> __ -> 'a1) -> 'a1
907
908val good_if_rect_Type5 :
909  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
910  -> __ -> 'a1) -> 'a1
911
912val good_if_rect_Type3 :
913  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
914  -> __ -> 'a1) -> 'a1
915
916val good_if_rect_Type2 :
917  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
918  -> __ -> 'a1) -> 'a1
919
920val good_if_rect_Type1 :
921  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
922  -> __ -> 'a1) -> 'a1
923
924val good_if_rect_Type0 :
925  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
926  -> __ -> 'a1) -> 'a1
927
928val good_if_inv_rect_Type4 :
929  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
930  -> __ -> __ -> 'a1) -> 'a1
931
932val good_if_inv_rect_Type3 :
933  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
934  -> __ -> __ -> 'a1) -> 'a1
935
936val good_if_inv_rect_Type2 :
937  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
938  -> __ -> __ -> 'a1) -> 'a1
939
940val good_if_inv_rect_Type1 :
941  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
942  -> __ -> __ -> 'a1) -> 'a1
943
944val good_if_inv_rect_Type0 :
945  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
946  -> __ -> __ -> 'a1) -> 'a1
947
948val good_if_discr :
949  params -> AST.ident List.list -> joint_internal_function -> __
950
951val good_if_jmdiscr :
952  params -> AST.ident List.list -> joint_internal_function -> __
953
954type joint_closed_internal_function = joint_internal_function Types.sig0
955
956val set_joint_code :
957  AST.ident List.list -> params -> joint_internal_function -> __ -> __
958  Types.sig0 -> joint_internal_function
959
960val set_joint_if_graph :
961  AST.ident List.list -> graph_params -> __ -> joint_internal_function ->
962  joint_internal_function
963
964val set_luniverse :
965  params -> AST.ident List.list -> joint_internal_function ->
966  Identifiers.universe -> joint_internal_function
967
968val set_runiverse :
969  params -> AST.ident List.list -> joint_internal_function ->
970  Identifiers.universe -> joint_internal_function
971
972val add_graph :
973  graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
974  joint_internal_function -> joint_internal_function
975
976type joint_function = joint_closed_internal_function AST.fundef
977
978type joint_program = (joint_function, Nat.nat) AST.program
979
980val lp_to_p__o__stmt_pars : graph_params -> stmt_params
Note: See TracBrowser for help on using the repository browser.