source: extracted/classifyOp.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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