source: extracted/classifyOp.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: 18.0 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
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.