source: extracted/classifyOp.ml @ 3009

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

New extraction.

File size: 40.1 KB
RevLine 
[2601]1open Preamble
2
3open CostLabel
4
[2649]5open Coqlib
6
[2601]7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
[2717]27open Exp
28
[2601]29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
[2773]35open Util
36
37open FoldStuff
38
39open BitVector
40
[2601]41open Jmeq
42
43open Russell
44
45open List
46
[2773]47open Setoids
[2601]48
[2773]49open Monad
[2601]50
[2773]51open Option
[2601]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 **)
[3001]98let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9258 x_9257 = function
[2601]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 **)
[3001]110let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9265 x_9264 = function
[2601]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 **)
[3001]122let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9272 x_9271 = function
[2601]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 **)
[3001]134let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9279 x_9278 = function
[2601]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 **)
[3001]146let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9286 x_9285 = function
[2601]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 **)
[3001]158let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_9293 x_9292 = function
[2601]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 **)
[3001]321let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9349 x_9348 = function
[2601]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 **)
[3001]333let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9356 x_9355 = function
[2601]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 **)
[3001]345let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9363 x_9362 = function
[2601]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 **)
[3001]357let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9370 x_9369 = function
[2601]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 **)
[3001]369let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9377 x_9376 = function
[2601]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 **)
[3001]381let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_9384 x_9383 = function
[2601]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 **)
[3001]521let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_9438 x_9437 = function
[2601]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 **)
[3001]528let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_9443 x_9442 = function
[2601]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 **)
[3001]535let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_9448 x_9447 = function
[2601]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 **)
[3001]542let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_9453 x_9452 = function
[2601]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 **)
[3001]549let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_9458 x_9457 = function
[2601]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 **)
[3001]556let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_9463 x_9462 = function
[2601]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 **)
[3001]638let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9504 x_9503 = function
[2601]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 **)
[3001]647let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9510 x_9509 = function
[2601]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 **)
[3001]656let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9516 x_9515 = function
[2601]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 **)
[3001]665let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9522 x_9521 = function
[2601]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 **)
[3001]674let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9528 x_9527 = function
[2601]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 **)
[3001]683let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_9534 x_9533 = function
[2601]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
[3001]782| Fun_case_f (x_9582, x_9581) -> h_fun_case_f x_9582 x_9581
[2601]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
[3001]789| Fun_case_f (x_9587, x_9586) -> h_fun_case_f x_9587 x_9586
[2601]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
[3001]796| Fun_case_f (x_9592, x_9591) -> h_fun_case_f x_9592 x_9591
[2601]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
[3001]803| Fun_case_f (x_9597, x_9596) -> h_fun_case_f x_9597 x_9596
[2601]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
[3001]810| Fun_case_f (x_9602, x_9601) -> h_fun_case_f x_9602 x_9601
[2601]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
[3001]817| Fun_case_f (x_9607, x_9606) -> h_fun_case_f x_9607 x_9606
[2601]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
[2773]876   | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
[2601]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
[2773]881| Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
[2601]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.