source: extracted/classifyOp.mli @ 2601

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

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

The extracted directory contains:

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

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

File size: 18.0 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Coqlib
30
31open Floats
32
33open Arithmetic
34
35open Char
36
37open String
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79open TypeComparison
80
81val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0
82
83type classify_add_cases =
84| Add_case_ii of AST.intsize * AST.signedness
85| Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
86   * AST.signedness
87| Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
88   * Csyntax.type0
89| Add_default of Csyntax.type0 * Csyntax.type0
90
91val classify_add_cases_rect_Type4 :
92  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
93  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
94  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
95  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
96  -> classify_add_cases -> 'a1
97
98val classify_add_cases_rect_Type5 :
99  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
100  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
101  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
102  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
103  -> classify_add_cases -> 'a1
104
105val classify_add_cases_rect_Type3 :
106  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
107  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
108  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
109  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
110  -> classify_add_cases -> 'a1
111
112val classify_add_cases_rect_Type2 :
113  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
114  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
115  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
116  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
117  -> classify_add_cases -> 'a1
118
119val classify_add_cases_rect_Type1 :
120  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
121  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
122  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
123  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
124  -> classify_add_cases -> 'a1
125
126val classify_add_cases_rect_Type0 :
127  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
128  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
129  Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
130  (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
131  -> classify_add_cases -> 'a1
132
133val classify_add_cases_inv_rect_Type4 :
134  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
135  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
136  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
137  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
138  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
139  -> 'a1) -> 'a1
140
141val classify_add_cases_inv_rect_Type3 :
142  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
143  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
144  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
145  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
146  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
147  -> 'a1) -> 'a1
148
149val classify_add_cases_inv_rect_Type2 :
150  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
151  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
152  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
153  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
154  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
155  -> 'a1) -> 'a1
156
157val classify_add_cases_inv_rect_Type1 :
158  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
159  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
160  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
161  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
162  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
163  -> 'a1) -> 'a1
164
165val classify_add_cases_inv_rect_Type0 :
166  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
167  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
168  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
169  (Nat.nat Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 ->
170  __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> __ -> __ -> __
171  -> 'a1) -> 'a1
172
173val classify_add_cases_discr :
174  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
175  -> __
176
177val classify_add_cases_jmdiscr :
178  Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> classify_add_cases
179  -> __
180
181val classify_add : Csyntax.type0 -> Csyntax.type0 -> classify_add_cases
182
183type classify_sub_cases =
184| Sub_case_ii of AST.intsize * AST.signedness
185| Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
186   * AST.signedness
187| Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
188   * Csyntax.type0
189| Sub_default of Csyntax.type0 * Csyntax.type0
190
191val classify_sub_cases_rect_Type4 :
192  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
193  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
194  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
195  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
196  Csyntax.type0 -> classify_sub_cases -> 'a1
197
198val classify_sub_cases_rect_Type5 :
199  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
200  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
201  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
202  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
203  Csyntax.type0 -> classify_sub_cases -> 'a1
204
205val classify_sub_cases_rect_Type3 :
206  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
207  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
208  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
209  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
210  Csyntax.type0 -> classify_sub_cases -> 'a1
211
212val classify_sub_cases_rect_Type2 :
213  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
214  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
215  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
216  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
217  Csyntax.type0 -> classify_sub_cases -> 'a1
218
219val classify_sub_cases_rect_Type1 :
220  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
221  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
222  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
223  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
224  Csyntax.type0 -> classify_sub_cases -> 'a1
225
226val classify_sub_cases_rect_Type0 :
227  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
228  Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
229  Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
230  'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
231  Csyntax.type0 -> classify_sub_cases -> 'a1
232
233val classify_sub_cases_inv_rect_Type4 :
234  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
235  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
236  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
237  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
238  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
239  -> __ -> __ -> __ -> 'a1) -> 'a1
240
241val classify_sub_cases_inv_rect_Type3 :
242  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
243  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
244  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
245  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
246  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
247  -> __ -> __ -> __ -> 'a1) -> 'a1
248
249val classify_sub_cases_inv_rect_Type2 :
250  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
251  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
252  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
253  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
254  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
255  -> __ -> __ -> __ -> 'a1) -> 'a1
256
257val classify_sub_cases_inv_rect_Type1 :
258  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
259  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
260  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
261  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
262  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
263  -> __ -> __ -> __ -> 'a1) -> 'a1
264
265val classify_sub_cases_inv_rect_Type0 :
266  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
267  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
268  Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
269  (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
270  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
271  -> __ -> __ -> __ -> 'a1) -> 'a1
272
273val classify_sub_cases_discr :
274  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
275  -> __
276
277val classify_sub_cases_jmdiscr :
278  Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> classify_sub_cases
279  -> __
280
281val classify_sub : Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases
282
283type classify_aop_cases =
284| Aop_case_ii of AST.intsize * AST.signedness
285| Aop_default of Csyntax.type0 * Csyntax.type0
286
287val classify_aop_cases_rect_Type4 :
288  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
289  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
290
291val classify_aop_cases_rect_Type5 :
292  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
293  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
294
295val classify_aop_cases_rect_Type3 :
296  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
297  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
298
299val classify_aop_cases_rect_Type2 :
300  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
301  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
302
303val classify_aop_cases_rect_Type1 :
304  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
305  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
306
307val classify_aop_cases_rect_Type0 :
308  (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
309  -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1
310
311val classify_aop_cases_inv_rect_Type4 :
312  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
313  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
314  -> __ -> __ -> __ -> 'a1) -> 'a1
315
316val classify_aop_cases_inv_rect_Type3 :
317  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
318  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
319  -> __ -> __ -> __ -> 'a1) -> 'a1
320
321val classify_aop_cases_inv_rect_Type2 :
322  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
323  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
324  -> __ -> __ -> __ -> 'a1) -> 'a1
325
326val classify_aop_cases_inv_rect_Type1 :
327  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
328  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
329  -> __ -> __ -> __ -> 'a1) -> 'a1
330
331val classify_aop_cases_inv_rect_Type0 :
332  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
333  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
334  -> __ -> __ -> __ -> 'a1) -> 'a1
335
336val classify_aop_cases_discr :
337  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
338  -> __
339
340val classify_aop_cases_jmdiscr :
341  Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> classify_aop_cases
342  -> __
343
344val classify_aop : Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases
345
346type classify_cmp_cases =
347| Cmp_case_ii of AST.intsize * AST.signedness
348| Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
349| Cmp_default of Csyntax.type0 * Csyntax.type0
350
351val classify_cmp_cases_rect_Type4 :
352  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
353  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
354  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
355
356val classify_cmp_cases_rect_Type5 :
357  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
358  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
359  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
360
361val classify_cmp_cases_rect_Type3 :
362  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
363  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
364  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
365
366val classify_cmp_cases_rect_Type2 :
367  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
368  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
369  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
370
371val classify_cmp_cases_rect_Type1 :
372  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
373  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
374  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
375
376val classify_cmp_cases_rect_Type0 :
377  (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
378  Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
379  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1
380
381val classify_cmp_cases_inv_rect_Type4 :
382  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
383  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
384  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
385  -> __ -> __ -> __ -> 'a1) -> 'a1
386
387val classify_cmp_cases_inv_rect_Type3 :
388  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
389  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
390  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
391  -> __ -> __ -> __ -> 'a1) -> 'a1
392
393val classify_cmp_cases_inv_rect_Type2 :
394  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
395  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
396  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
397  -> __ -> __ -> __ -> 'a1) -> 'a1
398
399val classify_cmp_cases_inv_rect_Type1 :
400  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
401  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
402  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
403  -> __ -> __ -> __ -> 'a1) -> 'a1
404
405val classify_cmp_cases_inv_rect_Type0 :
406  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
407  AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
408  Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
409  -> __ -> __ -> __ -> 'a1) -> 'a1
410
411val classify_cmp_cases_discr :
412  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
413  -> __
414
415val classify_cmp_cases_jmdiscr :
416  Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> classify_cmp_cases
417  -> __
418
419val classify_cmp : Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases
420
421type classify_fun_cases =
422| Fun_case_f of Csyntax.typelist * Csyntax.type0
423| Fun_default
424
425val classify_fun_cases_rect_Type4 :
426  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
427  'a1
428
429val classify_fun_cases_rect_Type5 :
430  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
431  'a1
432
433val classify_fun_cases_rect_Type3 :
434  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
435  'a1
436
437val classify_fun_cases_rect_Type2 :
438  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
439  'a1
440
441val classify_fun_cases_rect_Type1 :
442  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
443  'a1
444
445val classify_fun_cases_rect_Type0 :
446  (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases ->
447  'a1
448
449val classify_fun_cases_inv_rect_Type4 :
450  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
451  (__ -> 'a1) -> 'a1
452
453val classify_fun_cases_inv_rect_Type3 :
454  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
455  (__ -> 'a1) -> 'a1
456
457val classify_fun_cases_inv_rect_Type2 :
458  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
459  (__ -> 'a1) -> 'a1
460
461val classify_fun_cases_inv_rect_Type1 :
462  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
463  (__ -> 'a1) -> 'a1
464
465val classify_fun_cases_inv_rect_Type0 :
466  classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
467  (__ -> 'a1) -> 'a1
468
469val classify_fun_cases_discr : classify_fun_cases -> classify_fun_cases -> __
470
471val classify_fun_cases_jmdiscr :
472  classify_fun_cases -> classify_fun_cases -> __
473
474val classify_fun : Csyntax.type0 -> classify_fun_cases
475
Note: See TracBrowser for help on using the repository browser.