63 open Hints_declaration
79 (** val ptr_type : Csyntax.type0 -> Nat.nat Types.option -> Csyntax.type0 **)
80 let ptr_type ty = function
81 | Types.None -> Csyntax.Tpointer ty
82 | Types.Some n' -> Csyntax.Tarray (ty, n')
84 type 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
88 | Add_case_ip of Nat.nat Types.option * AST.intsize * AST.signedness
90 | Add_default of Csyntax.type0 * Csyntax.type0
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 **)
98 let rec classify_add_cases_rect_Type4 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7441 x_7440 = function
99 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
100 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
101 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
102 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
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 **)
110 let rec classify_add_cases_rect_Type5 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7448 x_7447 = function
111 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
112 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
113 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
114 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
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 **)
122 let rec classify_add_cases_rect_Type3 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7455 x_7454 = function
123 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
124 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
125 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
126 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
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 **)
134 let rec classify_add_cases_rect_Type2 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7462 x_7461 = function
135 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
136 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
137 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
138 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
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 **)
146 let rec classify_add_cases_rect_Type1 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7469 x_7468 = function
147 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
148 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
149 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
150 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
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 **)
158 let rec classify_add_cases_rect_Type0 h_add_case_ii h_add_case_pi h_add_case_ip h_add_default x_7476 x_7475 = function
159 | Add_case_ii (sz, sg) -> h_add_case_ii sz sg
160 | Add_case_pi (n, ty, sz, sg) -> h_add_case_pi n ty sz sg
161 | Add_case_ip (n, sz, sg, ty) -> h_add_case_ip n sz sg ty
162 | Add_default (ty1, ty2) -> h_add_default ty1 ty2
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 **)
171 let 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
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 **)
182 let 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
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 **)
193 let 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
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 **)
204 let 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
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 **)
215 let 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
219 (** val classify_add_cases_discr :
220 Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
221 classify_add_cases -> __ **)
222 let classify_add_cases_discr a1 a2 x y =
223 Logic.eq_rect_Type2 x
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
232 (** val classify_add_cases_jmdiscr :
233 Csyntax.type0 -> Csyntax.type0 -> classify_add_cases ->
234 classify_add_cases -> __ **)
235 let classify_add_cases_jmdiscr a1 a2 x y =
236 Logic.eq_rect_Type2 x
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
245 (** val classify_add :
246 Csyntax.type0 -> Csyntax.type0 -> classify_add_cases **)
247 let classify_add ty1 ty2 =
249 | Csyntax.Tvoid -> Add_default (Csyntax.Tvoid, ty2)
250 | Csyntax.Tint (sz1, sg1) ->
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 ->
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) ->
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,
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)
307 type 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
311 | Sub_case_pp of Nat.nat Types.option * Nat.nat Types.option * Csyntax.type0
313 | Sub_default of Csyntax.type0 * Csyntax.type0
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 **)
321 let rec classify_sub_cases_rect_Type4 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7532 x_7531 = function
322 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
323 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
324 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
325 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
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 **)
333 let rec classify_sub_cases_rect_Type5 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7539 x_7538 = function
334 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
335 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
336 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
337 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
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 **)
345 let rec classify_sub_cases_rect_Type3 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7546 x_7545 = function
346 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
347 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
348 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
349 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
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 **)
357 let rec classify_sub_cases_rect_Type2 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7553 x_7552 = function
358 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
359 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
360 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
361 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
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 **)
369 let rec classify_sub_cases_rect_Type1 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7560 x_7559 = function
370 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
371 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
372 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
373 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
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 **)
381 let rec classify_sub_cases_rect_Type0 h_sub_case_ii h_sub_case_pi h_sub_case_pp h_sub_default x_7567 x_7566 = function
382 | Sub_case_ii (sz, sg) -> h_sub_case_ii sz sg
383 | Sub_case_pi (n, ty, sz, sg) -> h_sub_case_pi n ty sz sg
384 | Sub_case_pp (n1, n2, ty1, ty2) -> h_sub_case_pp n1 n2 ty1 ty2
385 | Sub_default (ty1, ty2) -> h_sub_default ty1 ty2
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 **)
394 let 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
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 **)
405 let 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
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 **)
416 let 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
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 **)
427 let 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
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 **)
438 let 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
442 (** val classify_sub_cases_discr :
443 Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
444 classify_sub_cases -> __ **)
445 let classify_sub_cases_discr a1 a2 x y =
446 Logic.eq_rect_Type2 x
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
455 (** val classify_sub_cases_jmdiscr :
456 Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases ->
457 classify_sub_cases -> __ **)
458 let classify_sub_cases_jmdiscr a1 a2 x y =
459 Logic.eq_rect_Type2 x
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
468 (** val classify_sub :
469 Csyntax.type0 -> Csyntax.type0 -> classify_sub_cases **)
470 let classify_sub ty1 ty2 =
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 ->
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) ->
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,
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)
514 type classify_aop_cases =
515 | Aop_case_ii of AST.intsize * AST.signedness
516 | Aop_default of Csyntax.type0 * Csyntax.type0
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 **)
521 let rec classify_aop_cases_rect_Type4 h_aop_case_ii h_aop_default x_7621 x_7620 = function
522 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
523 | Aop_default (ty, ty') -> h_aop_default ty ty'
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 **)
528 let rec classify_aop_cases_rect_Type5 h_aop_case_ii h_aop_default x_7626 x_7625 = function
529 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
530 | Aop_default (ty, ty') -> h_aop_default ty ty'
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 **)
535 let rec classify_aop_cases_rect_Type3 h_aop_case_ii h_aop_default x_7631 x_7630 = function
536 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
537 | Aop_default (ty, ty') -> h_aop_default ty ty'
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 **)
542 let rec classify_aop_cases_rect_Type2 h_aop_case_ii h_aop_default x_7636 x_7635 = function
543 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
544 | Aop_default (ty, ty') -> h_aop_default ty ty'
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 **)
549 let rec classify_aop_cases_rect_Type1 h_aop_case_ii h_aop_default x_7641 x_7640 = function
550 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
551 | Aop_default (ty, ty') -> h_aop_default ty ty'
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 **)
556 let rec classify_aop_cases_rect_Type0 h_aop_case_ii h_aop_default x_7646 x_7645 = function
557 | Aop_case_ii (sz, sg) -> h_aop_case_ii sz sg
558 | Aop_default (ty, ty') -> h_aop_default ty ty'
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 **)
564 let 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 __ __ __
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 **)
571 let 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 __ __ __
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 **)
578 let 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 __ __ __
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 **)
585 let 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 __ __ __
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 **)
592 let 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 __ __ __
595 (** val classify_aop_cases_discr :
596 Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
597 classify_aop_cases -> __ **)
598 let classify_aop_cases_discr a1 a2 x y =
599 Logic.eq_rect_Type2 x
601 | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
602 | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
604 (** val classify_aop_cases_jmdiscr :
605 Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases ->
606 classify_aop_cases -> __ **)
607 let classify_aop_cases_jmdiscr a1 a2 x y =
608 Logic.eq_rect_Type2 x
610 | Aop_case_ii (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
611 | Aop_default (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
613 (** val classify_aop :
614 Csyntax.type0 -> Csyntax.type0 -> classify_aop_cases **)
615 let classify_aop ty1 ty2 =
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)
629 type 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
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 **)
638 let rec classify_cmp_cases_rect_Type4 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7687 x_7686 = function
639 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
640 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
641 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
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 **)
647 let rec classify_cmp_cases_rect_Type5 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7693 x_7692 = function
648 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
649 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
650 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
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 **)
656 let rec classify_cmp_cases_rect_Type3 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7699 x_7698 = function
657 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
658 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
659 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
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 **)
665 let rec classify_cmp_cases_rect_Type2 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7705 x_7704 = function
666 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
667 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
668 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
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 **)
674 let rec classify_cmp_cases_rect_Type1 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7711 x_7710 = function
675 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
676 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
677 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
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 **)
683 let rec classify_cmp_cases_rect_Type0 h_cmp_case_ii h_cmp_case_pp h_cmp_default x_7717 x_7716 = function
684 | Cmp_case_ii (sz, sg) -> h_cmp_case_ii sz sg
685 | Cmp_case_pp (n, ty) -> h_cmp_case_pp n ty
686 | Cmp_default (ty, ty') -> h_cmp_default ty ty'
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 **)
693 let 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
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 **)
702 let 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
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 **)
711 let 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
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 **)
720 let 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
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 **)
729 let 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
733 (** val classify_cmp_cases_discr :
734 Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
735 classify_cmp_cases -> __ **)
736 let classify_cmp_cases_discr a1 a2 x y =
737 Logic.eq_rect_Type2 x
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
743 (** val classify_cmp_cases_jmdiscr :
744 Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases ->
745 classify_cmp_cases -> __ **)
746 let classify_cmp_cases_jmdiscr a1 a2 x y =
747 Logic.eq_rect_Type2 x
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
753 (** val classify_cmp :
754 Csyntax.type0 -> Csyntax.type0 -> classify_cmp_cases **)
755 let classify_cmp ty1 ty2 =
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)),
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)
774 type classify_fun_cases =
775 | Fun_case_f of Csyntax.typelist * Csyntax.type0
778 (** val classify_fun_cases_rect_Type4 :
779 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
781 let rec classify_fun_cases_rect_Type4 h_fun_case_f h_fun_default = function
782 | Fun_case_f (x_7765, x_7764) -> h_fun_case_f x_7765 x_7764
783 | Fun_default -> h_fun_default
785 (** val classify_fun_cases_rect_Type5 :
786 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
788 let rec classify_fun_cases_rect_Type5 h_fun_case_f h_fun_default = function
789 | Fun_case_f (x_7770, x_7769) -> h_fun_case_f x_7770 x_7769
790 | Fun_default -> h_fun_default
792 (** val classify_fun_cases_rect_Type3 :
793 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
795 let rec classify_fun_cases_rect_Type3 h_fun_case_f h_fun_default = function
796 | Fun_case_f (x_7775, x_7774) -> h_fun_case_f x_7775 x_7774
797 | Fun_default -> h_fun_default
799 (** val classify_fun_cases_rect_Type2 :
800 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
802 let rec classify_fun_cases_rect_Type2 h_fun_case_f h_fun_default = function
803 | Fun_case_f (x_7780, x_7779) -> h_fun_case_f x_7780 x_7779
804 | Fun_default -> h_fun_default
806 (** val classify_fun_cases_rect_Type1 :
807 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
809 let rec classify_fun_cases_rect_Type1 h_fun_case_f h_fun_default = function
810 | Fun_case_f (x_7785, x_7784) -> h_fun_case_f x_7785 x_7784
811 | Fun_default -> h_fun_default
813 (** val classify_fun_cases_rect_Type0 :
814 (Csyntax.typelist -> Csyntax.type0 -> 'a1) -> 'a1 -> classify_fun_cases
816 let rec classify_fun_cases_rect_Type0 h_fun_case_f h_fun_default = function
817 | Fun_case_f (x_7790, x_7789) -> h_fun_case_f x_7790 x_7789
818 | Fun_default -> h_fun_default
820 (** val classify_fun_cases_inv_rect_Type4 :
821 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
822 (__ -> 'a1) -> 'a1 **)
823 let classify_fun_cases_inv_rect_Type4 hterm h1 h2 =
824 let hcut = classify_fun_cases_rect_Type4 h1 h2 hterm in hcut __
826 (** val classify_fun_cases_inv_rect_Type3 :
827 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
828 (__ -> 'a1) -> 'a1 **)
829 let classify_fun_cases_inv_rect_Type3 hterm h1 h2 =
830 let hcut = classify_fun_cases_rect_Type3 h1 h2 hterm in hcut __
832 (** val classify_fun_cases_inv_rect_Type2 :
833 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
834 (__ -> 'a1) -> 'a1 **)
835 let classify_fun_cases_inv_rect_Type2 hterm h1 h2 =
836 let hcut = classify_fun_cases_rect_Type2 h1 h2 hterm in hcut __
838 (** val classify_fun_cases_inv_rect_Type1 :
839 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
840 (__ -> 'a1) -> 'a1 **)
841 let classify_fun_cases_inv_rect_Type1 hterm h1 h2 =
842 let hcut = classify_fun_cases_rect_Type1 h1 h2 hterm in hcut __
844 (** val classify_fun_cases_inv_rect_Type0 :
845 classify_fun_cases -> (Csyntax.typelist -> Csyntax.type0 -> __ -> 'a1) ->
846 (__ -> 'a1) -> 'a1 **)
847 let classify_fun_cases_inv_rect_Type0 hterm h1 h2 =
848 let hcut = classify_fun_cases_rect_Type0 h1 h2 hterm in hcut __
850 (** val classify_fun_cases_discr :
851 classify_fun_cases -> classify_fun_cases -> __ **)
852 let classify_fun_cases_discr x y =
853 Logic.eq_rect_Type2 x
855 | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
856 | Fun_default -> Obj.magic (fun _ dH -> dH)) y
858 (** val classify_fun_cases_jmdiscr :
859 classify_fun_cases -> classify_fun_cases -> __ **)
860 let classify_fun_cases_jmdiscr x y =
861 Logic.eq_rect_Type2 x
863 | Fun_case_f (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
864 | Fun_default -> Obj.magic (fun _ dH -> dH)) y
866 (** val classify_fun : Csyntax.type0 -> classify_fun_cases **)
867 let classify_fun = function
868 | Csyntax.Tvoid -> Fun_default
869 | Csyntax.Tint (x, x0) -> Fun_default
870 | Csyntax.Tpointer ty' ->
872 | Csyntax.Tvoid -> Fun_default
873 | Csyntax.Tint (x, x0) -> Fun_default
874 | Csyntax.Tpointer x -> Fun_default
875 | Csyntax.Tarray (x, x0) -> Fun_default
876 | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
877 | Csyntax.Tstruct (x, x0) -> Fun_default
878 | Csyntax.Tunion (x, x0) -> Fun_default
879 | Csyntax.Tcomp_ptr x -> Fun_default)
880 | Csyntax.Tarray (x, x0) -> Fun_default
881 | Csyntax.Tfunction (args, res) -> Fun_case_f (args, res)
882 | Csyntax.Tstruct (x, x0) -> Fun_default
883 | Csyntax.Tunion (x, x0) -> Fun_default
884 | Csyntax.Tcomp_ptr x -> Fun_default