source: driver/extracted/classifyOp.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 40.1 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open TypeComparison
78
79(** val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0 **)
80let ptr_type ty = function
81| Types.None -> Csyntax.Tpointer ty
82| Types.Some n' -> Csyntax.Tarray (ty, n')
83
84type classify_add_cases =
85| Add_case_ii of AST.intsize * AST.signedness
86| Add_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
87   * AST.signedness
88| Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
89   * Csyntax.type0
90| Add_default of Csyntax.type0 * Csyntax.type0
91
92(** val classify_add_cases_rect_Type4 :
93    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
94    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
95    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
96    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
97    -> classify_add_cases -> 'a1 **)
98let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7441 x_7440 = function
99| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
100| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
101| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
102| Add_default (ty1, ty2) -> h_add_default ty1 ty2
103
104(** val classify_add_cases_rect_Type5 :
105    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
106    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
107    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
108    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
109    -> classify_add_cases -> 'a1 **)
110let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7448 x_7447 = function
111| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
112| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
113| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
114| Add_default (ty1, ty2) -> h_add_default ty1 ty2
115
116(** val classify_add_cases_rect_Type3 :
117    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
118    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
119    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
120    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
121    -> classify_add_cases -> 'a1 **)
122let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7455 x_7454 = function
123| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
124| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
125| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
126| Add_default (ty1, ty2) -> h_add_default ty1 ty2
127
128(** val classify_add_cases_rect_Type2 :
129    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
130    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
131    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
132    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
133    -> classify_add_cases -> 'a1 **)
134let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7462 x_7461 = function
135| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
136| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
137| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
138| Add_default (ty1, ty2) -> h_add_default ty1 ty2
139
140(** val classify_add_cases_rect_Type1 :
141    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
142    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
143    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
144    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
145    -> classify_add_cases -> 'a1 **)
146let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7469 x_7468 = function
147| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
148| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
149| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
150| Add_default (ty1, ty2) -> h_add_default ty1 ty2
151
152(** val classify_add_cases_rect_Type0 :
153    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
154    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
155    Types.option -> AST.intsize -> AST.signedness -> Csyntax.type0 -> 'a1) ->
156    (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 -> Csyntax.type0
157    -> classify_add_cases -> 'a1 **)
158let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7476 x_7475 = function
159| Add_case_ii (sz, sg) -> h_add_case_ii sz sg
160| Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
161| Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
162| Add_default (ty1, ty2) -> h_add_default ty1 ty2
163
164(** val classify_add_cases_inv_rect_Type4 :
165    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
166    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
167    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
168    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
169    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
170    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
171let classify_add_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
172  let hcut = classify_add_cases_rect_Type4 h1 h2 h3 h4 x1 x2 hterm in
173  hcut __ __ __
174
175(** val classify_add_cases_inv_rect_Type3 :
176    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
177    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
178    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
179    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
180    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
181    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
182let classify_add_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
183  let hcut = classify_add_cases_rect_Type3 h1 h2 h3 h4 x1 x2 hterm in
184  hcut __ __ __
185
186(** val classify_add_cases_inv_rect_Type2 :
187    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
188    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
189    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
190    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
191    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
192    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
193let classify_add_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
194  let hcut = classify_add_cases_rect_Type2 h1 h2 h3 h4 x1 x2 hterm in
195  hcut __ __ __
196
197(** val classify_add_cases_inv_rect_Type1 :
198    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
199    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
200    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
201    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
202    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
203    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
204let classify_add_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
205  let hcut = classify_add_cases_rect_Type1 h1 h2 h3 h4 x1 x2 hterm in
206  hcut __ __ __
207
208(** val classify_add_cases_inv_rect_Type0 :
209    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases -> (AST.intsize ->
210    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
211    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
212    -> (Nat.nat Types.option -> AST.intsize -> AST.signedness ->
213    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
214    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
215let classify_add_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
216  let hcut = classify_add_cases_rect_Type0 h1 h2 h3 h4 x1 x2 hterm in
217  hcut __ __ __
218
219(** val classify_add_cases_discr :
220    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
221    classify_add_cases -> __ **)
222let classify_add_cases_discr a1 a2 x y =
223  Logic.eq_rect_Type2 x
224    (match x with
225     | Add_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
226     | Add_case_pi (a0, a10, a20, a3) ->
227       Obj.magic (fun _ dH -> dH __ __ __ __)
228     | Add_case_ip (a0, a10, a20, a3) ->
229       Obj.magic (fun _ dH -> dH __ __ __ __)
230     | Add_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
231
232(** val classify_add_cases_jmdiscr :
233    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
234    classify_add_cases -> __ **)
235let classify_add_cases_jmdiscr a1 a2 x y =
236  Logic.eq_rect_Type2 x
237    (match x with
238     | Add_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
239     | Add_case_pi (a0, a10, a20, a3) ->
240       Obj.magic (fun _ dH -> dH __ __ __ __)
241     | Add_case_ip (a0, a10, a20, a3) ->
242       Obj.magic (fun _ dH -> dH __ __ __ __)
243     | Add_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
244
245(** val classify_add :
246    Csyntax.type0 -> Csyntax.type0 -> classify_add_cases **)
247let classify_add ty1 ty2 =
248  match ty1 with
249  | Csyntax.Tvoid -> Add_default (Csyntax.Tvoid, ty2)
250  | Csyntax.Tint (sz1, sg1) ->
251    (match ty2 with
252     | Csyntax.Tvoid ->
253       Add_default ((Csyntax.Tint (sz1, sg1)), Csyntax.Tvoid)
254     | Csyntax.Tint (sz2, sg2) ->
255       AST.inttyp_eq_elim' sz1 sz2 sg1 sg2 (Add_case_ii (sz1, sg1))
256         (Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tint (sz2, sg2))))
257     | Csyntax.Tpointer ty -> Add_case_ip (Types.None, sz1, sg1, ty)
258     | Csyntax.Tarray (ty, n) -> Add_case_ip ((Types.Some n), sz1, sg1, ty)
259     | Csyntax.Tfunction (x, x0) ->
260       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tfunction (x, x0)))
261     | Csyntax.Tstruct (x, x0) ->
262       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tstruct (x, x0)))
263     | Csyntax.Tunion (x, x0) ->
264       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tunion (x, x0)))
265     | Csyntax.Tcomp_ptr x ->
266       Add_default ((Csyntax.Tint (sz1, sg1)), (Csyntax.Tcomp_ptr x)))
267  | Csyntax.Tpointer ty ->
268    (match ty2 with
269     | Csyntax.Tvoid -> Add_default ((ptr_type ty Types.None), Csyntax.Tvoid)
270     | Csyntax.Tint (x, x0) -> Add_case_pi (Types.None, ty, x, x0)
271     | Csyntax.Tpointer x ->
272       Add_default ((ptr_type ty Types.None), (Csyntax.Tpointer x))
273     | Csyntax.Tarray (x, x0) ->
274       Add_default ((ptr_type ty Types.None), (Csyntax.Tarray (x, x0)))
275     | Csyntax.Tfunction (x, x0) ->
276       Add_default ((ptr_type ty Types.None), (Csyntax.Tfunction (x, x0)))
277     | Csyntax.Tstruct (x, x0) ->
278       Add_default ((ptr_type ty Types.None), (Csyntax.Tstruct (x, x0)))
279     | Csyntax.Tunion (x, x0) ->
280       Add_default ((ptr_type ty Types.None), (Csyntax.Tunion (x, x0)))
281     | Csyntax.Tcomp_ptr x ->
282       Add_default ((ptr_type ty Types.None), (Csyntax.Tcomp_ptr x)))
283  | Csyntax.Tarray (ty, n) ->
284    (match ty2 with
285     | Csyntax.Tvoid ->
286       Add_default ((ptr_type ty (Types.Some n)), Csyntax.Tvoid)
287     | Csyntax.Tint (x, x0) -> Add_case_pi ((Types.Some n), ty, x, x0)
288     | Csyntax.Tpointer x ->
289       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tpointer x))
290     | Csyntax.Tarray (x, x0) ->
291       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tarray (x, x0)))
292     | Csyntax.Tfunction (x, x0) ->
293       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tfunction (x,
294         x0)))
295     | Csyntax.Tstruct (x, x0) ->
296       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tstruct (x, x0)))
297     | Csyntax.Tunion (x, x0) ->
298       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tunion (x, x0)))
299     | Csyntax.Tcomp_ptr x ->
300       Add_default ((ptr_type ty (Types.Some n)), (Csyntax.Tcomp_ptr x)))
301  | Csyntax.Tfunction (x, x0) ->
302    Add_default ((Csyntax.Tfunction (x, x0)), ty2)
303  | Csyntax.Tstruct (x, x0) -> Add_default ((Csyntax.Tstruct (x, x0)), ty2)
304  | Csyntax.Tunion (x, x0) -> Add_default ((Csyntax.Tunion (x, x0)), ty2)
305  | Csyntax.Tcomp_ptr x -> Add_default ((Csyntax.Tcomp_ptr x), ty2)
306
307type classify_sub_cases =
308| Sub_case_ii of AST.intsize * AST.signedness
309| Sub_case_pi of Nat.nat Types.option * Csyntax.type0 * AST.intsize
310   * AST.signedness
311| Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
312   * Csyntax.type0
313| Sub_default of Csyntax.type0 * Csyntax.type0
314
315(** val classify_sub_cases_rect_Type4 :
316    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
317    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
318    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
319    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
320    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
321let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7532 x_7531 = function
322| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
323| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
324| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
325| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
326
327(** val classify_sub_cases_rect_Type5 :
328    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
329    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
330    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
331    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
332    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
333let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7539 x_7538 = function
334| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
335| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
336| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
337| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
338
339(** val classify_sub_cases_rect_Type3 :
340    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
341    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
342    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
343    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
344    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
345let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7546 x_7545 = function
346| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
347| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
348| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
349| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
350
351(** val classify_sub_cases_rect_Type2 :
352    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
353    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
354    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
355    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
356    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
357let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7553 x_7552 = function
358| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
359| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
360| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
361| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
362
363(** val classify_sub_cases_rect_Type1 :
364    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
365    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
366    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
367    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
368    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
369let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7560 x_7559 = function
370| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
371| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
372| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
373| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
374
375(** val classify_sub_cases_rect_Type0 :
376    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
377    Csyntax.type0 -> AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat
378    Types.option -> Nat.nat Types.option -> Csyntax.type0 -> Csyntax.type0 ->
379    'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) -> Csyntax.type0 ->
380    Csyntax.type0 -> classify_sub_cases -> 'a1 **)
381let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7567 x_7566 = function
382| Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
383| Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
384| Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
385| Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
386
387(** val classify_sub_cases_inv_rect_Type4 :
388    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
389    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
390    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
391    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
392    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
393    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
394let classify_sub_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 h4 =
395  let hcut = classify_sub_cases_rect_Type4 h1 h2 h3 h4 x1 x2 hterm in
396  hcut __ __ __
397
398(** val classify_sub_cases_inv_rect_Type3 :
399    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
400    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
401    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
402    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
403    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
404    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
405let classify_sub_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 h4 =
406  let hcut = classify_sub_cases_rect_Type3 h1 h2 h3 h4 x1 x2 hterm in
407  hcut __ __ __
408
409(** val classify_sub_cases_inv_rect_Type2 :
410    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
411    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
412    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
413    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
414    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
415    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
416let classify_sub_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 h4 =
417  let hcut = classify_sub_cases_rect_Type2 h1 h2 h3 h4 x1 x2 hterm in
418  hcut __ __ __
419
420(** val classify_sub_cases_inv_rect_Type1 :
421    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
422    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
423    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
424    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
425    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
426    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
427let classify_sub_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 h4 =
428  let hcut = classify_sub_cases_rect_Type1 h1 h2 h3 h4 x1 x2 hterm in
429  hcut __ __ __
430
431(** val classify_sub_cases_inv_rect_Type0 :
432    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases -> (AST.intsize ->
433    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
434    Csyntax.type0 -> AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1)
435    -> (Nat.nat Types.option -> Nat.nat Types.option -> Csyntax.type0 ->
436    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
437    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
438let classify_sub_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 h4 =
439  let hcut = classify_sub_cases_rect_Type0 h1 h2 h3 h4 x1 x2 hterm in
440  hcut __ __ __
441
442(** val classify_sub_cases_discr :
443    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
444    classify_sub_cases -> __ **)
445let classify_sub_cases_discr a1 a2 x y =
446  Logic.eq_rect_Type2 x
447    (match x with
448     | Sub_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
449     | Sub_case_pi (a0, a10, a20, a3) ->
450       Obj.magic (fun _ dH -> dH __ __ __ __)
451     | Sub_case_pp (a0, a10, a20, a3) ->
452       Obj.magic (fun _ dH -> dH __ __ __ __)
453     | Sub_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
454
455(** val classify_sub_cases_jmdiscr :
456    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
457    classify_sub_cases -> __ **)
458let classify_sub_cases_jmdiscr a1 a2 x y =
459  Logic.eq_rect_Type2 x
460    (match x with
461     | Sub_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
462     | Sub_case_pi (a0, a10, a20, a3) ->
463       Obj.magic (fun _ dH -> dH __ __ __ __)
464     | Sub_case_pp (a0, a10, a20, a3) ->
465       Obj.magic (fun _ dH -> dH __ __ __ __)
466     | Sub_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
467
468(** val classify_sub :
469    Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases **)
470let classify_sub ty1 ty2 =
471  match ty1 with
472  | Csyntax.Tvoid -> Sub_default (Csyntax.Tvoid, ty2)
473  | Csyntax.Tint (sz1, sg1) ->
474    TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Sub_case_ii
475      (sz1, sg1)) (Sub_default ((Csyntax.Tint (sz1, sg1)), ty2))
476  | Csyntax.Tpointer ty ->
477    (match ty2 with
478     | Csyntax.Tvoid -> Sub_default ((ptr_type ty Types.None), Csyntax.Tvoid)
479     | Csyntax.Tint (sz, sg) -> Sub_case_pi (Types.None, ty, sz, sg)
480     | Csyntax.Tpointer x -> Sub_case_pp (Types.None, Types.None, ty, x)
481     | Csyntax.Tarray (x, n2) ->
482       Sub_case_pp (Types.None, (Types.Some n2), ty, x)
483     | Csyntax.Tfunction (x, x0) ->
484       Sub_default ((ptr_type ty Types.None), (Csyntax.Tfunction (x, x0)))
485     | Csyntax.Tstruct (x, x0) ->
486       Sub_default ((ptr_type ty Types.None), (Csyntax.Tstruct (x, x0)))
487     | Csyntax.Tunion (x, x0) ->
488       Sub_default ((ptr_type ty Types.None), (Csyntax.Tunion (x, x0)))
489     | Csyntax.Tcomp_ptr x ->
490       Sub_default ((ptr_type ty Types.None), (Csyntax.Tcomp_ptr x)))
491  | Csyntax.Tarray (ty, n1) ->
492    (match ty2 with
493     | Csyntax.Tvoid ->
494       Sub_default ((ptr_type ty (Types.Some n1)), Csyntax.Tvoid)
495     | Csyntax.Tint (x, x0) -> Sub_case_pi ((Types.Some n1), ty, x, x0)
496     | Csyntax.Tpointer x -> Sub_case_pp ((Types.Some n1), Types.None, ty, x)
497     | Csyntax.Tarray (x, n2) ->
498       Sub_case_pp ((Types.Some n1), (Types.Some n2), ty, x)
499     | Csyntax.Tfunction (x, x0) ->
500       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tfunction (x,
501         x0)))
502     | Csyntax.Tstruct (x, x0) ->
503       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tstruct (x, x0)))
504     | Csyntax.Tunion (x, x0) ->
505       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tunion (x, x0)))
506     | Csyntax.Tcomp_ptr x ->
507       Sub_default ((ptr_type ty (Types.Some n1)), (Csyntax.Tcomp_ptr x)))
508  | Csyntax.Tfunction (x, x0) ->
509    Sub_default ((Csyntax.Tfunction (x, x0)), ty2)
510  | Csyntax.Tstruct (x, x0) -> Sub_default ((Csyntax.Tstruct (x, x0)), ty2)
511  | Csyntax.Tunion (x, x0) -> Sub_default ((Csyntax.Tunion (x, x0)), ty2)
512  | Csyntax.Tcomp_ptr x -> Sub_default ((Csyntax.Tcomp_ptr x), ty2)
513
514type classify_aop_cases =
515| Aop_case_ii of AST.intsize * AST.signedness
516| Aop_default of Csyntax.type0 * Csyntax.type0
517
518(** val classify_aop_cases_rect_Type4 :
519    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
520    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
521let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7621 x_7620 = function
522| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
523| Aop_default (ty, ty') -> h_aop_default ty ty'
524
525(** val classify_aop_cases_rect_Type5 :
526    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
527    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
528let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7626 x_7625 = function
529| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
530| Aop_default (ty, ty') -> h_aop_default ty ty'
531
532(** val classify_aop_cases_rect_Type3 :
533    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
534    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
535let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7631 x_7630 = function
536| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
537| Aop_default (ty, ty') -> h_aop_default ty ty'
538
539(** val classify_aop_cases_rect_Type2 :
540    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
541    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
542let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7636 x_7635 = function
543| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
544| Aop_default (ty, ty') -> h_aop_default ty ty'
545
546(** val classify_aop_cases_rect_Type1 :
547    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
548    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
549let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7641 x_7640 = function
550| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
551| Aop_default (ty, ty') -> h_aop_default ty ty'
552
553(** val classify_aop_cases_rect_Type0 :
554    (AST.intsize -> AST.signedness -> 'a1) -> (Csyntax.type0 -> Csyntax.type0
555    -> 'a1) -> Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> 'a1 **)
556let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7646 x_7645 = function
557| Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
558| Aop_default (ty, ty') -> h_aop_default ty ty'
559
560(** val classify_aop_cases_inv_rect_Type4 :
561    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
562    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
563    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
564let classify_aop_cases_inv_rect_Type4 x1 x2 hterm h1 h2 =
565  let hcut = classify_aop_cases_rect_Type4 h1 h2 x1 x2 hterm in hcut __ __ __
566
567(** val classify_aop_cases_inv_rect_Type3 :
568    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
569    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
570    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
571let classify_aop_cases_inv_rect_Type3 x1 x2 hterm h1 h2 =
572  let hcut = classify_aop_cases_rect_Type3 h1 h2 x1 x2 hterm in hcut __ __ __
573
574(** val classify_aop_cases_inv_rect_Type2 :
575    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
576    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
577    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
578let classify_aop_cases_inv_rect_Type2 x1 x2 hterm h1 h2 =
579  let hcut = classify_aop_cases_rect_Type2 h1 h2 x1 x2 hterm in hcut __ __ __
580
581(** val classify_aop_cases_inv_rect_Type1 :
582    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
583    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
584    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
585let classify_aop_cases_inv_rect_Type1 x1 x2 hterm h1 h2 =
586  let hcut = classify_aop_cases_rect_Type1 h1 h2 x1 x2 hterm in hcut __ __ __
587
588(** val classify_aop_cases_inv_rect_Type0 :
589    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases -> (AST.intsize ->
590    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
591    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
592let classify_aop_cases_inv_rect_Type0 x1 x2 hterm h1 h2 =
593  let hcut = classify_aop_cases_rect_Type0 h1 h2 x1 x2 hterm in hcut __ __ __
594
595(** val classify_aop_cases_discr :
596    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
597    classify_aop_cases -> __ **)
598let classify_aop_cases_discr a1 a2 x y =
599  Logic.eq_rect_Type2 x
600    (match x with
601     | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
602     | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
603
604(** val classify_aop_cases_jmdiscr :
605    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
606    classify_aop_cases -> __ **)
607let classify_aop_cases_jmdiscr a1 a2 x y =
608  Logic.eq_rect_Type2 x
609    (match x with
610     | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
611     | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
612
613(** val classify_aop :
614    Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases **)
615let classify_aop ty1 ty2 =
616  match ty1 with
617  | Csyntax.Tvoid -> Aop_default (Csyntax.Tvoid, ty2)
618  | Csyntax.Tint (sz1, sg1) ->
619    TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Aop_case_ii
620      (sz1, sg1)) (Aop_default ((Csyntax.Tint (sz1, sg1)), ty2))
621  | Csyntax.Tpointer x -> Aop_default ((Csyntax.Tpointer x), ty2)
622  | Csyntax.Tarray (x, x0) -> Aop_default ((Csyntax.Tarray (x, x0)), ty2)
623  | Csyntax.Tfunction (x, x0) ->
624    Aop_default ((Csyntax.Tfunction (x, x0)), ty2)
625  | Csyntax.Tstruct (x, x0) -> Aop_default ((Csyntax.Tstruct (x, x0)), ty2)
626  | Csyntax.Tunion (x, x0) -> Aop_default ((Csyntax.Tunion (x, x0)), ty2)
627  | Csyntax.Tcomp_ptr x -> Aop_default ((Csyntax.Tcomp_ptr x), ty2)
628
629type classify_cmp_cases =
630| Cmp_case_ii of AST.intsize * AST.signedness
631| Cmp_case_pp of Nat.nat Types.option * Csyntax.type0
632| Cmp_default of Csyntax.type0 * Csyntax.type0
633
634(** val classify_cmp_cases_rect_Type4 :
635    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
636    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
637    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
638let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7687 x_7686 = function
639| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
640| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
641| Cmp_default (ty, ty') -> h_cmp_default ty ty'
642
643(** val classify_cmp_cases_rect_Type5 :
644    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
645    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
646    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
647let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7693 x_7692 = function
648| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
649| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
650| Cmp_default (ty, ty') -> h_cmp_default ty ty'
651
652(** val classify_cmp_cases_rect_Type3 :
653    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
654    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
655    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
656let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7699 x_7698 = function
657| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
658| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
659| Cmp_default (ty, ty') -> h_cmp_default ty ty'
660
661(** val classify_cmp_cases_rect_Type2 :
662    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
663    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
664    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
665let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7705 x_7704 = function
666| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
667| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
668| Cmp_default (ty, ty') -> h_cmp_default ty ty'
669
670(** val classify_cmp_cases_rect_Type1 :
671    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
672    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
673    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
674let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7711 x_7710 = function
675| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
676| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
677| Cmp_default (ty, ty') -> h_cmp_default ty ty'
678
679(** val classify_cmp_cases_rect_Type0 :
680    (AST.intsize -> AST.signedness -> 'a1) -> (Nat.nat Types.option ->
681    Csyntax.type0 -> 'a1) -> (Csyntax.type0 -> Csyntax.type0 -> 'a1) ->
682    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> 'a1 **)
683let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7717 x_7716 = function
684| Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
685| Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
686| Cmp_default (ty, ty') -> h_cmp_default ty ty'
687
688(** val classify_cmp_cases_inv_rect_Type4 :
689    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
690    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
691    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
692    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
693let classify_cmp_cases_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
694  let hcut = classify_cmp_cases_rect_Type4 h1 h2 h3 x1 x2 hterm in
695  hcut __ __ __
696
697(** val classify_cmp_cases_inv_rect_Type3 :
698    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
699    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
700    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
701    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
702let classify_cmp_cases_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
703  let hcut = classify_cmp_cases_rect_Type3 h1 h2 h3 x1 x2 hterm in
704  hcut __ __ __
705
706(** val classify_cmp_cases_inv_rect_Type2 :
707    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
708    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
709    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
710    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
711let classify_cmp_cases_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
712  let hcut = classify_cmp_cases_rect_Type2 h1 h2 h3 x1 x2 hterm in
713  hcut __ __ __
714
715(** val classify_cmp_cases_inv_rect_Type1 :
716    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
717    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
718    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
719    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
720let classify_cmp_cases_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
721  let hcut = classify_cmp_cases_rect_Type1 h1 h2 h3 x1 x2 hterm in
722  hcut __ __ __
723
724(** val classify_cmp_cases_inv_rect_Type0 :
725    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases -> (AST.intsize ->
726    AST.signedness -> __ -> __ -> __ -> 'a1) -> (Nat.nat Types.option ->
727    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> (Csyntax.type0 ->
728    Csyntax.type0 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
729let classify_cmp_cases_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
730  let hcut = classify_cmp_cases_rect_Type0 h1 h2 h3 x1 x2 hterm in
731  hcut __ __ __
732
733(** val classify_cmp_cases_discr :
734    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
735    classify_cmp_cases -> __ **)
736let classify_cmp_cases_discr a1 a2 x y =
737  Logic.eq_rect_Type2 x
738    (match x with
739     | Cmp_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
740     | Cmp_case_pp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
741     | Cmp_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
742
743(** val classify_cmp_cases_jmdiscr :
744    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
745    classify_cmp_cases -> __ **)
746let classify_cmp_cases_jmdiscr a1 a2 x y =
747  Logic.eq_rect_Type2 x
748    (match x with
749     | Cmp_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
750     | Cmp_case_pp (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
751     | Cmp_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
752
753(** val classify_cmp :
754    Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases **)
755let classify_cmp ty1 ty2 =
756  match ty1 with
757  | Csyntax.Tvoid -> Cmp_default (Csyntax.Tvoid, ty2)
758  | Csyntax.Tint (sz1, sg1) ->
759    TypeComparison.if_type_eq (Csyntax.Tint (sz1, sg1)) ty2 (Cmp_case_ii
760      (sz1, sg1)) (Cmp_default ((Csyntax.Tint (sz1, sg1)), ty2))
761  | Csyntax.Tpointer ty1' ->
762    TypeComparison.if_type_eq (Csyntax.Tpointer ty1') ty2 (Cmp_case_pp
763      (Types.None, ty1')) (Cmp_default ((Csyntax.Tpointer ty1'), ty2))
764  | Csyntax.Tarray (ty1', n1) ->
765    TypeComparison.if_type_eq (Csyntax.Tarray (ty1', n1)) ty2 (Cmp_case_pp
766      ((Types.Some n1), ty1')) (Cmp_default ((Csyntax.Tarray (ty1', n1)),
767      ty2))
768  | Csyntax.Tfunction (x, x0) ->
769    Cmp_default ((Csyntax.Tfunction (x, x0)), ty2)
770  | Csyntax.Tstruct (x, x0) -> Cmp_default ((Csyntax.Tstruct (x, x0)), ty2)
771  | Csyntax.Tunion (x, x0) -> Cmp_default ((Csyntax.Tunion (x, x0)), ty2)
772  | Csyntax.Tcomp_ptr x -> Cmp_default ((Csyntax.Tcomp_ptr x), ty2)
773
774type classify_fun_cases =
775| Fun_case_f of Csyntax.typelist * Csyntax.type0
776| Fun_default
777
778(** val classify_fun_cases_rect_Type4 :
779    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
780    -> 'a1 **)
781let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
782| Fun_case_f (x_7765, x_7764) -> h_fun_case_f x_7765 x_7764
783| Fun_default -> h_fun_default
784
785(** val classify_fun_cases_rect_Type5 :
786    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
787    -> 'a1 **)
788let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
789| Fun_case_f (x_7770, x_7769) -> h_fun_case_f x_7770 x_7769
790| Fun_default -> h_fun_default
791
792(** val classify_fun_cases_rect_Type3 :
793    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
794    -> 'a1 **)
795let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
796| Fun_case_f (x_7775, x_7774) -> h_fun_case_f x_7775 x_7774
797| Fun_default -> h_fun_default
798
799(** val classify_fun_cases_rect_Type2 :
800    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
801    -> 'a1 **)
802let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
803| Fun_case_f (x_7780, x_7779) -> h_fun_case_f x_7780 x_7779
804| Fun_default -> h_fun_default
805
806(** val classify_fun_cases_rect_Type1 :
807    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
808    -> 'a1 **)
809let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
810| Fun_case_f (x_7785, x_7784) -> h_fun_case_f x_7785 x_7784
811| Fun_default -> h_fun_default
812
813(** val classify_fun_cases_rect_Type0 :
814    (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
815    -> 'a1 **)
816let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
817| Fun_case_f (x_7790, x_7789) -> h_fun_case_f x_7790 x_7789
818| Fun_default -> h_fun_default
819
820(** val classify_fun_cases_inv_rect_Type4 :
821    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
822    (__ -> 'a1) -> 'a1 **)
823let classify_fun_cases_inv_rect_Type4 hterm h1 h2 =
824  let hcut = classify_fun_cases_rect_Type4 h1 h2 hterm in hcut __
825
826(** val classify_fun_cases_inv_rect_Type3 :
827    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
828    (__ -> 'a1) -> 'a1 **)
829let classify_fun_cases_inv_rect_Type3 hterm h1 h2 =
830  let hcut = classify_fun_cases_rect_Type3 h1 h2 hterm in hcut __
831
832(** val classify_fun_cases_inv_rect_Type2 :
833    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
834    (__ -> 'a1) -> 'a1 **)
835let classify_fun_cases_inv_rect_Type2 hterm h1 h2 =
836  let hcut = classify_fun_cases_rect_Type2 h1 h2 hterm in hcut __
837
838(** val classify_fun_cases_inv_rect_Type1 :
839    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
840    (__ -> 'a1) -> 'a1 **)
841let classify_fun_cases_inv_rect_Type1 hterm h1 h2 =
842  let hcut = classify_fun_cases_rect_Type1 h1 h2 hterm in hcut __
843
844(** val classify_fun_cases_inv_rect_Type0 :
845    classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
846    (__ -> 'a1) -> 'a1 **)
847let classify_fun_cases_inv_rect_Type0 hterm h1 h2 =
848  let hcut = classify_fun_cases_rect_Type0 h1 h2 hterm in hcut __
849
850(** val classify_fun_cases_discr :
851    classify_fun_cases -> classify_fun_cases -> __ **)
852let classify_fun_cases_discr x y =
853  Logic.eq_rect_Type2 x
854    (match x with
855     | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
856     | Fun_default -> Obj.magic (fun _ dH -> dH)) y
857
858(** val classify_fun_cases_jmdiscr :
859    classify_fun_cases -> classify_fun_cases -> __ **)
860let classify_fun_cases_jmdiscr x y =
861  Logic.eq_rect_Type2 x
862    (match x with
863     | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
864     | Fun_default -> Obj.magic (fun _ dH -> dH)) y
865
866(** val classify_fun : Csyntax.type0 -> classify_fun_cases **)
867let classify_fun = function
868| Csyntax.Tvoid -> Fun_default
869| Csyntax.Tint (x, x0) -> Fun_default
870| Csyntax.Tpointer ty' ->
871  (match ty' with
872   | Csyntax.Tvoid -> Fun_default
873   | Csyntax.Tint (x, x0) -> Fun_default
874   | Csyntax.Tpointer x -> Fun_default
875   | Csyntax.Tarray (x, x0) -> Fun_default
876   | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
877   | Csyntax.Tstruct (x, x0) -> Fun_default
878   | Csyntax.Tunion (x, x0) -> Fun_default
879   | Csyntax.Tcomp_ptr x -> Fun_default)
880| Csyntax.Tarray (x, x0) -> Fun_default
881| Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
882| Csyntax.Tstruct (x, x0) -> Fun_default
883| Csyntax.Tunion (x, x0) -> Fun_default
884| Csyntax.Tcomp_ptr x -> Fun_default
885
Note: See TracBrowser for help on using the repository browser.