source: extracted/joint.mli @ 2743

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 38.3 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 dpi1__o__reg_to_psd_argument__o__inject :
151  (Registers.register, 'a1) Types.dPair -> psd_argument Types.sig0
152
153val eject__o__reg_to_psd_argument__o__inject :
154  Registers.register Types.sig0 -> psd_argument Types.sig0
155
156val reg_to_psd_argument__o__inject :
157  Registers.register -> psd_argument Types.sig0
158
159val dpi1__o__reg_to_psd_argument :
160  (Registers.register, 'a1) Types.dPair -> psd_argument
161
162val eject__o__reg_to_psd_argument :
163  Registers.register Types.sig0 -> psd_argument
164
165val psd_argument_from_byte : BitVector.byte -> psd_argument
166
167val dpi1__o__byte_to_psd_argument__o__inject :
168  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
169
170val eject__o__byte_to_psd_argument__o__inject :
171  BitVector.byte Types.sig0 -> psd_argument Types.sig0
172
173val byte_to_psd_argument__o__inject :
174  BitVector.byte -> psd_argument Types.sig0
175
176val dpi1__o__byte_to_psd_argument :
177  (BitVector.byte, 'a1) Types.dPair -> psd_argument
178
179val eject__o__byte_to_psd_argument :
180  BitVector.byte Types.sig0 -> psd_argument
181
182type hdw_argument = I8051.register argument
183
184val hdw_argument_from_reg : I8051.register -> hdw_argument
185
186val dpi1__o__reg_to_hdw_argument__o__inject :
187  (I8051.register, 'a1) Types.dPair -> hdw_argument Types.sig0
188
189val eject__o__reg_to_hdw_argument__o__inject :
190  I8051.register Types.sig0 -> hdw_argument Types.sig0
191
192val reg_to_hdw_argument__o__inject :
193  I8051.register -> hdw_argument Types.sig0
194
195val dpi1__o__reg_to_hdw_argument :
196  (I8051.register, 'a1) Types.dPair -> hdw_argument
197
198val eject__o__reg_to_hdw_argument : I8051.register Types.sig0 -> hdw_argument
199
200val hdw_argument_from_byte : BitVector.byte -> hdw_argument
201
202val dpi1__o__byte_to_hdw_argument__o__inject :
203  (BitVector.byte, 'a1) Types.dPair -> psd_argument Types.sig0
204
205val eject__o__byte_to_hdw_argument__o__inject :
206  BitVector.byte Types.sig0 -> psd_argument Types.sig0
207
208val byte_to_hdw_argument__o__inject :
209  BitVector.byte -> psd_argument Types.sig0
210
211val dpi1__o__byte_to_hdw_argument :
212  (BitVector.byte, 'a1) Types.dPair -> psd_argument
213
214val eject__o__byte_to_hdw_argument :
215  BitVector.byte Types.sig0 -> psd_argument
216
217val byte_of_nat : Nat.nat -> BitVector.byte
218
219val zero_byte : BitVector.byte
220
221type unserialized_params = { ext_seq_labels : (__ -> Graphs.label List.list);
222                             has_tailcalls : Bool.bool }
223
224val unserialized_params_rect_Type4 :
225  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
226  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
227  unserialized_params -> 'a1
228
229val unserialized_params_rect_Type5 :
230  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
231  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
232  unserialized_params -> 'a1
233
234val unserialized_params_rect_Type3 :
235  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
236  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
237  unserialized_params -> 'a1
238
239val unserialized_params_rect_Type2 :
240  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
241  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
242  unserialized_params -> 'a1
243
244val unserialized_params_rect_Type1 :
245  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
246  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
247  unserialized_params -> 'a1
248
249val unserialized_params_rect_Type0 :
250  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
251  -> (__ -> Graphs.label List.list) -> Bool.bool -> __ -> 'a1) ->
252  unserialized_params -> 'a1
253
254type acc_a_reg
255
256type acc_b_reg
257
258type acc_a_arg
259
260type acc_b_arg
261
262type dpl_reg
263
264type dph_reg
265
266type dpl_arg
267
268type dph_arg
269
270type snd_arg
271
272type pair_move
273
274type call_args
275
276type call_dest
277
278type ext_seq
279
280val ext_seq_labels : unserialized_params -> __ -> Graphs.label List.list
281
282val has_tailcalls : unserialized_params -> Bool.bool
283
284type paramsT
285
286val unserialized_params_inv_rect_Type4 :
287  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
288  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
289  __ -> __ -> 'a1) -> 'a1
290
291val unserialized_params_inv_rect_Type3 :
292  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
293  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
294  __ -> __ -> 'a1) -> 'a1
295
296val unserialized_params_inv_rect_Type2 :
297  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
298  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
299  __ -> __ -> 'a1) -> 'a1
300
301val unserialized_params_inv_rect_Type1 :
302  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
303  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
304  __ -> __ -> 'a1) -> 'a1
305
306val unserialized_params_inv_rect_Type0 :
307  unserialized_params -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
308  -> __ -> __ -> __ -> __ -> (__ -> Graphs.label List.list) -> Bool.bool ->
309  __ -> __ -> 'a1) -> 'a1
310
311val unserialized_params_jmdiscr :
312  unserialized_params -> unserialized_params -> __
313
314type joint_seq =
315| COMMENT of String.string
316| MOVE of __
317| POP of __
318| PUSH of __
319| ADDRESS of AST.ident * __ * __
320| OPACCS of BackEndOps.opAccs * __ * __ * __ * __
321| OP1 of BackEndOps.op1 * __ * __
322| OP2 of BackEndOps.op2 * __ * __ * __
323| CLEAR_CARRY
324| SET_CARRY
325| LOAD of __ * __ * __
326| STORE of __ * __ * __
327| Extension_seq of __
328
329val joint_seq_rect_Type4 :
330  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
331  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
332  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
333  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
334  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
335  (__ -> 'a1) -> joint_seq -> 'a1
336
337val joint_seq_rect_Type5 :
338  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
339  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
340  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
341  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
342  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
343  (__ -> 'a1) -> joint_seq -> 'a1
344
345val joint_seq_rect_Type3 :
346  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
347  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
348  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
349  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
350  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
351  (__ -> 'a1) -> joint_seq -> 'a1
352
353val joint_seq_rect_Type2 :
354  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
355  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
356  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
357  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
358  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
359  (__ -> 'a1) -> joint_seq -> 'a1
360
361val joint_seq_rect_Type1 :
362  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
363  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
364  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
365  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
366  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
367  (__ -> 'a1) -> joint_seq -> 'a1
368
369val joint_seq_rect_Type0 :
370  unserialized_params -> AST.ident List.list -> (String.string -> 'a1) -> (__
371  -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (AST.ident -> __ -> __ -> __ ->
372  'a1) -> (BackEndOps.opAccs -> __ -> __ -> __ -> __ -> 'a1) ->
373  (BackEndOps.op1 -> __ -> __ -> 'a1) -> (BackEndOps.op2 -> __ -> __ -> __ ->
374  'a1) -> 'a1 -> 'a1 -> (__ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> 'a1) ->
375  (__ -> 'a1) -> joint_seq -> 'a1
376
377val joint_seq_inv_rect_Type4 :
378  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
379  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
380  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
381  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
382  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
383  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
384  'a1) -> (__ -> __ -> 'a1) -> 'a1
385
386val joint_seq_inv_rect_Type3 :
387  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
388  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
389  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
390  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
391  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
392  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
393  'a1) -> (__ -> __ -> 'a1) -> 'a1
394
395val joint_seq_inv_rect_Type2 :
396  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
397  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
398  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
399  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
400  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
401  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
402  'a1) -> (__ -> __ -> 'a1) -> 'a1
403
404val joint_seq_inv_rect_Type1 :
405  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
406  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
407  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
408  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
409  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
410  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
411  'a1) -> (__ -> __ -> 'a1) -> 'a1
412
413val joint_seq_inv_rect_Type0 :
414  unserialized_params -> AST.ident List.list -> joint_seq -> (String.string
415  -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ -> 'a1) -> (__ -> __ ->
416  'a1) -> (AST.ident -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.opAccs ->
417  __ -> __ -> __ -> __ -> __ -> 'a1) -> (BackEndOps.op1 -> __ -> __ -> __ ->
418  'a1) -> (BackEndOps.op2 -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> 'a1) ->
419  (__ -> 'a1) -> (__ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
420  'a1) -> (__ -> __ -> 'a1) -> 'a1
421
422val joint_seq_discr :
423  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
424
425val joint_seq_jmdiscr :
426  unserialized_params -> AST.ident List.list -> joint_seq -> joint_seq -> __
427
428val nOOP : unserialized_params -> AST.ident List.list -> joint_seq
429
430val dpi1__o__extension_seq_to_seq__o__inject :
431  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
432  joint_seq Types.sig0
433
434val eject__o__extension_seq_to_seq__o__inject :
435  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
436  Types.sig0
437
438val extension_seq_to_seq__o__inject :
439  unserialized_params -> AST.ident List.list -> __ -> joint_seq Types.sig0
440
441val dpi1__o__extension_seq_to_seq :
442  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
443  joint_seq
444
445val eject__o__extension_seq_to_seq :
446  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_seq
447
448type joint_step =
449| COST_LABEL of CostLabel.costlabel
450| CALL of (AST.ident, (__, __) Types.prod) Types.sum * __ * __
451| COND of __ * Graphs.label
452| Step_seq of joint_seq
453
454val joint_step_rect_Type4 :
455  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
456  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
457  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
458
459val joint_step_rect_Type5 :
460  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
461  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
462  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
463
464val joint_step_rect_Type3 :
465  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
466  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
467  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
468
469val joint_step_rect_Type2 :
470  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
471  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
472  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
473
474val joint_step_rect_Type1 :
475  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
476  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
477  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
478
479val joint_step_rect_Type0 :
480  unserialized_params -> AST.ident List.list -> (CostLabel.costlabel -> 'a1)
481  -> ((AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ -> 'a1) -> (__
482  -> Graphs.label -> 'a1) -> (joint_seq -> 'a1) -> joint_step -> 'a1
483
484val joint_step_inv_rect_Type4 :
485  unserialized_params -> AST.ident List.list -> joint_step ->
486  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
487  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
488  (joint_seq -> __ -> 'a1) -> 'a1
489
490val joint_step_inv_rect_Type3 :
491  unserialized_params -> AST.ident List.list -> joint_step ->
492  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
493  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
494  (joint_seq -> __ -> 'a1) -> 'a1
495
496val joint_step_inv_rect_Type2 :
497  unserialized_params -> AST.ident List.list -> joint_step ->
498  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
499  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
500  (joint_seq -> __ -> 'a1) -> 'a1
501
502val joint_step_inv_rect_Type1 :
503  unserialized_params -> AST.ident List.list -> joint_step ->
504  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
505  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
506  (joint_seq -> __ -> 'a1) -> 'a1
507
508val joint_step_inv_rect_Type0 :
509  unserialized_params -> AST.ident List.list -> joint_step ->
510  (CostLabel.costlabel -> __ -> 'a1) -> ((AST.ident, (__, __) Types.prod)
511  Types.sum -> __ -> __ -> __ -> 'a1) -> (__ -> Graphs.label -> __ -> 'a1) ->
512  (joint_seq -> __ -> 'a1) -> 'a1
513
514val joint_step_discr :
515  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
516  __
517
518val joint_step_jmdiscr :
519  unserialized_params -> AST.ident List.list -> joint_step -> joint_step ->
520  __
521
522val dpi1__o__extension_seq_to_seq__o__seq_to_step__o__inject :
523  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
524  joint_step Types.sig0
525
526val eject__o__extension_seq_to_seq__o__seq_to_step__o__inject :
527  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
528  Types.sig0
529
530val extension_seq_to_seq__o__seq_to_step__o__inject :
531  unserialized_params -> AST.ident List.list -> __ -> joint_step Types.sig0
532
533val dpi1__o__seq_to_step__o__inject :
534  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
535  -> joint_step Types.sig0
536
537val eject__o__seq_to_step__o__inject :
538  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
539  joint_step Types.sig0
540
541val seq_to_step__o__inject :
542  unserialized_params -> AST.ident List.list -> joint_seq -> joint_step
543  Types.sig0
544
545val dpi1__o__extension_seq_to_seq__o__seq_to_step :
546  unserialized_params -> AST.ident List.list -> (__, 'a1) Types.dPair ->
547  joint_step
548
549val eject__o__extension_seq_to_seq__o__seq_to_step :
550  unserialized_params -> AST.ident List.list -> __ Types.sig0 -> joint_step
551
552val extension_seq_to_seq__o__seq_to_step :
553  unserialized_params -> AST.ident List.list -> __ -> joint_step
554
555val dpi1__o__seq_to_step :
556  unserialized_params -> AST.ident List.list -> (joint_seq, 'a1) Types.dPair
557  -> joint_step
558
559val eject__o__seq_to_step :
560  unserialized_params -> AST.ident List.list -> joint_seq Types.sig0 ->
561  joint_step
562
563val step_labels :
564  unserialized_params -> AST.ident List.list -> joint_step -> Graphs.label
565  List.list
566
567type stmt_params = { uns_pars : unserialized_params;
568                     succ_label : (__ -> Graphs.label Types.option);
569                     has_fcond : Bool.bool }
570
571val stmt_params_rect_Type4 :
572  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
573  Bool.bool -> 'a1) -> stmt_params -> 'a1
574
575val stmt_params_rect_Type5 :
576  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
577  Bool.bool -> 'a1) -> stmt_params -> 'a1
578
579val stmt_params_rect_Type3 :
580  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
581  Bool.bool -> 'a1) -> stmt_params -> 'a1
582
583val stmt_params_rect_Type2 :
584  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
585  Bool.bool -> 'a1) -> stmt_params -> 'a1
586
587val stmt_params_rect_Type1 :
588  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
589  Bool.bool -> 'a1) -> stmt_params -> 'a1
590
591val stmt_params_rect_Type0 :
592  (unserialized_params -> __ -> (__ -> Graphs.label Types.option) ->
593  Bool.bool -> 'a1) -> stmt_params -> 'a1
594
595val uns_pars : stmt_params -> unserialized_params
596
597type succ0
598
599val succ_label : stmt_params -> __ -> Graphs.label Types.option
600
601val has_fcond : stmt_params -> Bool.bool
602
603val stmt_params_inv_rect_Type4 :
604  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
605  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
606
607val stmt_params_inv_rect_Type3 :
608  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
609  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
610
611val stmt_params_inv_rect_Type2 :
612  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
613  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
614
615val stmt_params_inv_rect_Type1 :
616  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
617  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
618
619val stmt_params_inv_rect_Type0 :
620  stmt_params -> (unserialized_params -> __ -> (__ -> Graphs.label
621  Types.option) -> Bool.bool -> __ -> 'a1) -> 'a1
622
623val stmt_params_jmdiscr : stmt_params -> stmt_params -> __
624
625type joint_fin_step =
626| GOTO of Graphs.label
627| RETURN
628| TAILCALL of (AST.ident, (__, __) Types.prod) Types.sum * __
629
630val joint_fin_step_rect_Type4 :
631  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
632  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
633
634val joint_fin_step_rect_Type5 :
635  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
636  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
637
638val joint_fin_step_rect_Type3 :
639  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
640  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
641
642val joint_fin_step_rect_Type2 :
643  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
644  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
645
646val joint_fin_step_rect_Type1 :
647  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
648  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
649
650val joint_fin_step_rect_Type0 :
651  unserialized_params -> (Graphs.label -> 'a1) -> 'a1 -> (__ -> (AST.ident,
652  (__, __) Types.prod) Types.sum -> __ -> 'a1) -> joint_fin_step -> 'a1
653
654val joint_fin_step_inv_rect_Type4 :
655  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
656  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
657  'a1) -> 'a1
658
659val joint_fin_step_inv_rect_Type3 :
660  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
661  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
662  'a1) -> 'a1
663
664val joint_fin_step_inv_rect_Type2 :
665  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
666  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
667  'a1) -> 'a1
668
669val joint_fin_step_inv_rect_Type1 :
670  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
671  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
672  'a1) -> 'a1
673
674val joint_fin_step_inv_rect_Type0 :
675  unserialized_params -> joint_fin_step -> (Graphs.label -> __ -> 'a1) -> (__
676  -> 'a1) -> (__ -> (AST.ident, (__, __) Types.prod) Types.sum -> __ -> __ ->
677  'a1) -> 'a1
678
679val joint_fin_step_discr :
680  unserialized_params -> joint_fin_step -> joint_fin_step -> __
681
682val joint_fin_step_jmdiscr :
683  unserialized_params -> joint_fin_step -> joint_fin_step -> __
684
685val fin_step_labels :
686  unserialized_params -> joint_fin_step -> Graphs.label List.list
687
688type joint_statement =
689| Sequential of joint_step * __
690| Final of joint_fin_step
691| FCOND of __ * Graphs.label * Graphs.label
692
693val joint_statement_rect_Type4 :
694  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
695  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
696  'a1) -> joint_statement -> 'a1
697
698val joint_statement_rect_Type5 :
699  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
700  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
701  'a1) -> joint_statement -> 'a1
702
703val joint_statement_rect_Type3 :
704  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
705  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
706  'a1) -> joint_statement -> 'a1
707
708val joint_statement_rect_Type2 :
709  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
710  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
711  'a1) -> joint_statement -> 'a1
712
713val joint_statement_rect_Type1 :
714  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
715  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
716  'a1) -> joint_statement -> 'a1
717
718val joint_statement_rect_Type0 :
719  stmt_params -> AST.ident List.list -> (joint_step -> __ -> 'a1) ->
720  (joint_fin_step -> 'a1) -> (__ -> __ -> Graphs.label -> Graphs.label ->
721  'a1) -> joint_statement -> 'a1
722
723val joint_statement_inv_rect_Type4 :
724  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
725  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
726  -> Graphs.label -> __ -> 'a1) -> 'a1
727
728val joint_statement_inv_rect_Type3 :
729  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
730  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
731  -> Graphs.label -> __ -> 'a1) -> 'a1
732
733val joint_statement_inv_rect_Type2 :
734  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
735  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
736  -> Graphs.label -> __ -> 'a1) -> 'a1
737
738val joint_statement_inv_rect_Type1 :
739  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
740  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
741  -> Graphs.label -> __ -> 'a1) -> 'a1
742
743val joint_statement_inv_rect_Type0 :
744  stmt_params -> AST.ident List.list -> joint_statement -> (joint_step -> __
745  -> __ -> 'a1) -> (joint_fin_step -> __ -> 'a1) -> (__ -> __ -> Graphs.label
746  -> Graphs.label -> __ -> 'a1) -> 'a1
747
748val joint_statement_discr :
749  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
750  __
751
752val joint_statement_jmdiscr :
753  stmt_params -> AST.ident List.list -> joint_statement -> joint_statement ->
754  __
755
756val dpi1__o__fin_step_to_stmt__o__inject :
757  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
758  joint_statement Types.sig0
759
760val eject__o__fin_step_to_stmt__o__inject :
761  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
762  joint_statement Types.sig0
763
764val fin_step_to_stmt__o__inject :
765  stmt_params -> AST.ident List.list -> joint_fin_step -> joint_statement
766  Types.sig0
767
768val dpi1__o__fin_step_to_stmt :
769  stmt_params -> AST.ident List.list -> (joint_fin_step, 'a1) Types.dPair ->
770  joint_statement
771
772val eject__o__fin_step_to_stmt :
773  stmt_params -> AST.ident List.list -> joint_fin_step Types.sig0 ->
774  joint_statement
775
776type params = { stmt_pars : stmt_params;
777                stmt_at : (AST.ident List.list -> __ -> __ -> joint_statement
778                          Types.option);
779                point_of_label : (AST.ident List.list -> __ -> Graphs.label
780                                 -> __ Types.option);
781                point_of_succ : (__ -> __ -> __) }
782
783val params_rect_Type4 :
784  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
785  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
786  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
787
788val params_rect_Type5 :
789  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
790  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
791  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
792
793val params_rect_Type3 :
794  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
795  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
796  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
797
798val params_rect_Type2 :
799  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
800  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
801  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
802
803val params_rect_Type1 :
804  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
805  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
806  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
807
808val params_rect_Type0 :
809  (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
810  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
811  -> __ Types.option) -> (__ -> __ -> __) -> 'a1) -> params -> 'a1
812
813val stmt_pars : params -> stmt_params
814
815type codeT
816
817type code_point
818
819val stmt_at :
820  params -> AST.ident List.list -> __ -> __ -> joint_statement Types.option
821
822val point_of_label :
823  params -> AST.ident List.list -> __ -> Graphs.label -> __ Types.option
824
825val point_of_succ : params -> __ -> __ -> __
826
827val params_inv_rect_Type4 :
828  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
829  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
830  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
831
832val params_inv_rect_Type3 :
833  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
834  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
835  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
836
837val params_inv_rect_Type2 :
838  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
839  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
840  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
841
842val params_inv_rect_Type1 :
843  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
844  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
845  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
846
847val params_inv_rect_Type0 :
848  params -> (stmt_params -> __ -> __ -> (AST.ident List.list -> __ -> __ ->
849  joint_statement Types.option) -> (AST.ident List.list -> __ -> Graphs.label
850  -> __ Types.option) -> (__ -> __ -> __) -> __ -> 'a1) -> 'a1
851
852val params_jmdiscr : params -> params -> __
853
854val stmt_pars__o__uns_pars : params -> unserialized_params
855
856val code_has_point : params -> AST.ident List.list -> __ -> __ -> Bool.bool
857
858val code_has_label :
859  params -> AST.ident List.list -> __ -> Graphs.label -> Bool.bool
860
861val stmt_explicit_labels :
862  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
863  List.list
864
865val stmt_implicit_label :
866  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
867  Types.option
868
869val stmt_labels :
870  stmt_params -> AST.ident List.list -> joint_statement -> Graphs.label
871  List.list
872
873type lin_params =
874  unserialized_params
875  (* singleton inductive, whose constructor was mk_lin_params *)
876
877val lin_params_rect_Type4 : (unserialized_params -> 'a1) -> lin_params -> 'a1
878
879val lin_params_rect_Type5 : (unserialized_params -> 'a1) -> lin_params -> 'a1
880
881val lin_params_rect_Type3 : (unserialized_params -> 'a1) -> lin_params -> 'a1
882
883val lin_params_rect_Type2 : (unserialized_params -> 'a1) -> lin_params -> 'a1
884
885val lin_params_rect_Type1 : (unserialized_params -> 'a1) -> lin_params -> 'a1
886
887val lin_params_rect_Type0 : (unserialized_params -> 'a1) -> lin_params -> 'a1
888
889val l_u_pars : lin_params -> unserialized_params
890
891val lin_params_inv_rect_Type4 :
892  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
893
894val lin_params_inv_rect_Type3 :
895  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
896
897val lin_params_inv_rect_Type2 :
898  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
899
900val lin_params_inv_rect_Type1 :
901  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
902
903val lin_params_inv_rect_Type0 :
904  lin_params -> (unserialized_params -> __ -> 'a1) -> 'a1
905
906val lin_params_jmdiscr : lin_params -> lin_params -> __
907
908val lin_params_to_params : lin_params -> params
909
910val lp_to_p__o__stmt_pars : lin_params -> stmt_params
911
912val lp_to_p__o__stmt_pars__o__uns_pars : lin_params -> unserialized_params
913
914type graph_params =
915  unserialized_params
916  (* singleton inductive, whose constructor was mk_graph_params *)
917
918val graph_params_rect_Type4 :
919  (unserialized_params -> 'a1) -> graph_params -> 'a1
920
921val graph_params_rect_Type5 :
922  (unserialized_params -> 'a1) -> graph_params -> 'a1
923
924val graph_params_rect_Type3 :
925  (unserialized_params -> 'a1) -> graph_params -> 'a1
926
927val graph_params_rect_Type2 :
928  (unserialized_params -> 'a1) -> graph_params -> 'a1
929
930val graph_params_rect_Type1 :
931  (unserialized_params -> 'a1) -> graph_params -> 'a1
932
933val graph_params_rect_Type0 :
934  (unserialized_params -> 'a1) -> graph_params -> 'a1
935
936val g_u_pars : graph_params -> unserialized_params
937
938val graph_params_inv_rect_Type4 :
939  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
940
941val graph_params_inv_rect_Type3 :
942  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
943
944val graph_params_inv_rect_Type2 :
945  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
946
947val graph_params_inv_rect_Type1 :
948  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
949
950val graph_params_inv_rect_Type0 :
951  graph_params -> (unserialized_params -> __ -> 'a1) -> 'a1
952
953val graph_params_jmdiscr : graph_params -> graph_params -> __
954
955val graph_params_to_params : graph_params -> params
956
957val gp_to_p__o__stmt_pars : graph_params -> stmt_params
958
959val gp_to_p__o__stmt_pars__o__uns_pars : graph_params -> unserialized_params
960
961type joint_internal_function = { joint_if_luniverse : Identifiers.universe;
962                                 joint_if_runiverse : Identifiers.universe;
963                                 joint_if_result : __; joint_if_params : 
964                                 __; joint_if_stacksize : Nat.nat;
965                                 joint_if_code : __;
966                                 joint_if_entry : __ Types.sig0 }
967
968val joint_internal_function_rect_Type4 :
969  params -> AST.ident List.list -> (Identifiers.universe ->
970  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
971  -> joint_internal_function -> 'a1
972
973val joint_internal_function_rect_Type5 :
974  params -> AST.ident List.list -> (Identifiers.universe ->
975  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
976  -> joint_internal_function -> 'a1
977
978val joint_internal_function_rect_Type3 :
979  params -> AST.ident List.list -> (Identifiers.universe ->
980  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
981  -> joint_internal_function -> 'a1
982
983val joint_internal_function_rect_Type2 :
984  params -> AST.ident List.list -> (Identifiers.universe ->
985  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
986  -> joint_internal_function -> 'a1
987
988val joint_internal_function_rect_Type1 :
989  params -> AST.ident List.list -> (Identifiers.universe ->
990  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
991  -> joint_internal_function -> 'a1
992
993val joint_internal_function_rect_Type0 :
994  params -> AST.ident List.list -> (Identifiers.universe ->
995  Identifiers.universe -> __ -> __ -> Nat.nat -> __ -> __ Types.sig0 -> 'a1)
996  -> joint_internal_function -> 'a1
997
998val joint_if_luniverse :
999  params -> AST.ident List.list -> joint_internal_function ->
1000  Identifiers.universe
1001
1002val joint_if_runiverse :
1003  params -> AST.ident List.list -> joint_internal_function ->
1004  Identifiers.universe
1005
1006val joint_if_result :
1007  params -> AST.ident List.list -> joint_internal_function -> __
1008
1009val joint_if_params :
1010  params -> AST.ident List.list -> joint_internal_function -> __
1011
1012val joint_if_stacksize :
1013  params -> AST.ident List.list -> joint_internal_function -> Nat.nat
1014
1015val joint_if_code :
1016  params -> AST.ident List.list -> joint_internal_function -> __
1017
1018val joint_if_entry :
1019  params -> AST.ident List.list -> joint_internal_function -> __ Types.sig0
1020
1021val joint_internal_function_inv_rect_Type4 :
1022  params -> AST.ident List.list -> joint_internal_function ->
1023  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
1024  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
1025
1026val joint_internal_function_inv_rect_Type3 :
1027  params -> AST.ident List.list -> joint_internal_function ->
1028  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
1029  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
1030
1031val joint_internal_function_inv_rect_Type2 :
1032  params -> AST.ident List.list -> joint_internal_function ->
1033  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
1034  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
1035
1036val joint_internal_function_inv_rect_Type1 :
1037  params -> AST.ident List.list -> joint_internal_function ->
1038  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
1039  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
1040
1041val joint_internal_function_inv_rect_Type0 :
1042  params -> AST.ident List.list -> joint_internal_function ->
1043  (Identifiers.universe -> Identifiers.universe -> __ -> __ -> Nat.nat -> __
1044  -> __ Types.sig0 -> __ -> 'a1) -> 'a1
1045
1046val joint_internal_function_jmdiscr :
1047  params -> AST.ident List.list -> joint_internal_function ->
1048  joint_internal_function -> __
1049
1050val good_if_rect_Type4 :
1051  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1052  -> __ -> 'a1) -> 'a1
1053
1054val good_if_rect_Type5 :
1055  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1056  -> __ -> 'a1) -> 'a1
1057
1058val good_if_rect_Type3 :
1059  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1060  -> __ -> 'a1) -> 'a1
1061
1062val good_if_rect_Type2 :
1063  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1064  -> __ -> 'a1) -> 'a1
1065
1066val good_if_rect_Type1 :
1067  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1068  -> __ -> 'a1) -> 'a1
1069
1070val good_if_rect_Type0 :
1071  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1072  -> __ -> 'a1) -> 'a1
1073
1074val good_if_inv_rect_Type4 :
1075  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1076  -> __ -> __ -> 'a1) -> 'a1
1077
1078val good_if_inv_rect_Type3 :
1079  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1080  -> __ -> __ -> 'a1) -> 'a1
1081
1082val good_if_inv_rect_Type2 :
1083  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1084  -> __ -> __ -> 'a1) -> 'a1
1085
1086val good_if_inv_rect_Type1 :
1087  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1088  -> __ -> __ -> 'a1) -> 'a1
1089
1090val good_if_inv_rect_Type0 :
1091  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
1092  -> __ -> __ -> 'a1) -> 'a1
1093
1094val good_if_discr :
1095  params -> AST.ident List.list -> joint_internal_function -> __
1096
1097val good_if_jmdiscr :
1098  params -> AST.ident List.list -> joint_internal_function -> __
1099
1100type joint_closed_internal_function = joint_internal_function Types.sig0
1101
1102val set_joint_code :
1103  AST.ident List.list -> params -> joint_internal_function -> __ -> __
1104  Types.sig0 -> joint_internal_function
1105
1106val set_joint_if_graph :
1107  AST.ident List.list -> graph_params -> __ -> joint_internal_function ->
1108  joint_internal_function
1109
1110val set_luniverse :
1111  params -> AST.ident List.list -> joint_internal_function ->
1112  Identifiers.universe -> joint_internal_function
1113
1114val set_runiverse :
1115  params -> AST.ident List.list -> joint_internal_function ->
1116  Identifiers.universe -> joint_internal_function
1117
1118val add_graph :
1119  graph_params -> AST.ident List.list -> Graphs.label -> joint_statement ->
1120  joint_internal_function -> joint_internal_function
1121
1122type joint_function = joint_closed_internal_function AST.fundef
1123
1124type joint_program = (joint_function, Nat.nat) AST.program
1125
Note: See TracBrowser for help on using the repository browser.