source: extracted/classifyOp.ml @ 2649

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

...

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