59 open Hints_declaration
77 | Tint of AST.intsize * AST.signedness
79 | Tarray of type0 * Nat.nat
80 | Tfunction of typelist * type0
81 | Tstruct of AST.ident * fieldlist
82 | Tunion of AST.ident * fieldlist
83 | Tcomp_ptr of AST.ident
86 | Tcons of type0 * typelist
89 | Fcons of AST.ident * type0 * fieldlist
91 (** val type_inv_rect_Type4 :
92 type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
93 (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
94 type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
95 (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
96 let type_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
100 | Tint (x, x0) -> h2 x x0
102 | Tarray (x, x0) -> h4 x x0
103 | Tfunction (x, x0) -> h5 x x0
104 | Tstruct (x, x0) -> h6 x x0
105 | Tunion (x, x0) -> h7 x x0
106 | Tcomp_ptr x -> h8 x
110 (** val type_inv_rect_Type3 :
111 type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
112 (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
113 type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
114 (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
115 let type_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
119 | Tint (x, x0) -> h2 x x0
121 | Tarray (x, x0) -> h4 x x0
122 | Tfunction (x, x0) -> h5 x x0
123 | Tstruct (x, x0) -> h6 x x0
124 | Tunion (x, x0) -> h7 x x0
125 | Tcomp_ptr x -> h8 x
129 (** val type_inv_rect_Type2 :
130 type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
131 (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
132 type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
133 (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
134 let type_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
138 | Tint (x, x0) -> h2 x x0
140 | Tarray (x, x0) -> h4 x x0
141 | Tfunction (x, x0) -> h5 x x0
142 | Tstruct (x, x0) -> h6 x x0
143 | Tunion (x, x0) -> h7 x x0
144 | Tcomp_ptr x -> h8 x
148 (** val type_inv_rect_Type1 :
149 type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
150 (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
151 type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
152 (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
153 let type_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
157 | Tint (x, x0) -> h2 x x0
159 | Tarray (x, x0) -> h4 x x0
160 | Tfunction (x, x0) -> h5 x x0
161 | Tstruct (x, x0) -> h6 x x0
162 | Tunion (x, x0) -> h7 x x0
163 | Tcomp_ptr x -> h8 x
167 (** val type_inv_rect_Type0 :
168 type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
169 (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
170 type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) ->
171 (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
172 let type_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
176 | Tint (x, x0) -> h2 x x0
178 | Tarray (x, x0) -> h4 x x0
179 | Tfunction (x, x0) -> h5 x x0
180 | Tstruct (x, x0) -> h6 x x0
181 | Tunion (x, x0) -> h7 x x0
182 | Tcomp_ptr x -> h8 x
186 (** val typelist_inv_rect_Type4 :
187 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
188 let typelist_inv_rect_Type4 hterm h1 h2 =
192 | Tcons (x, x0) -> h2 x x0
196 (** val typelist_inv_rect_Type3 :
197 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
198 let typelist_inv_rect_Type3 hterm h1 h2 =
202 | Tcons (x, x0) -> h2 x x0
206 (** val typelist_inv_rect_Type2 :
207 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
208 let typelist_inv_rect_Type2 hterm h1 h2 =
212 | Tcons (x, x0) -> h2 x x0
216 (** val typelist_inv_rect_Type1 :
217 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
218 let typelist_inv_rect_Type1 hterm h1 h2 =
222 | Tcons (x, x0) -> h2 x x0
226 (** val typelist_inv_rect_Type0 :
227 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1 **)
228 let typelist_inv_rect_Type0 hterm h1 h2 =
232 | Tcons (x, x0) -> h2 x x0
236 (** val fieldlist_inv_rect_Type4 :
237 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
239 let fieldlist_inv_rect_Type4 hterm h1 h2 =
243 | Fcons (x, x0, x1) -> h2 x x0 x1
247 (** val fieldlist_inv_rect_Type3 :
248 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
250 let fieldlist_inv_rect_Type3 hterm h1 h2 =
254 | Fcons (x, x0, x1) -> h2 x x0 x1
258 (** val fieldlist_inv_rect_Type2 :
259 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
261 let fieldlist_inv_rect_Type2 hterm h1 h2 =
265 | Fcons (x, x0, x1) -> h2 x x0 x1
269 (** val fieldlist_inv_rect_Type1 :
270 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
272 let fieldlist_inv_rect_Type1 hterm h1 h2 =
276 | Fcons (x, x0, x1) -> h2 x x0 x1
280 (** val fieldlist_inv_rect_Type0 :
281 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ ->
283 let fieldlist_inv_rect_Type0 hterm h1 h2 =
287 | Fcons (x, x0, x1) -> h2 x x0 x1
291 (** val type_discr : type0 -> type0 -> __ **)
293 Logic.eq_rect_Type2 x
295 | Tvoid -> Obj.magic (fun _ dH -> dH)
296 | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
297 | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
298 | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
299 | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
300 | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
301 | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
302 | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y
304 (** val typelist_discr : typelist -> typelist -> __ **)
305 let typelist_discr x y =
306 Logic.eq_rect_Type2 x
308 | Tnil -> Obj.magic (fun _ dH -> dH)
309 | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
311 (** val fieldlist_discr : fieldlist -> fieldlist -> __ **)
312 let fieldlist_discr x y =
313 Logic.eq_rect_Type2 x
315 | Fnil -> Obj.magic (fun _ dH -> dH)
316 | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
318 (** val type_jmdiscr : type0 -> type0 -> __ **)
319 let type_jmdiscr x y =
320 Logic.eq_rect_Type2 x
322 | Tvoid -> Obj.magic (fun _ dH -> dH)
323 | Tint (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
324 | Tpointer a0 -> Obj.magic (fun _ dH -> dH __)
325 | Tarray (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
326 | Tfunction (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
327 | Tstruct (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
328 | Tunion (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
329 | Tcomp_ptr a0 -> Obj.magic (fun _ dH -> dH __)) y
331 (** val typelist_jmdiscr : typelist -> typelist -> __ **)
332 let typelist_jmdiscr x y =
333 Logic.eq_rect_Type2 x
335 | Tnil -> Obj.magic (fun _ dH -> dH)
336 | Tcons (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
338 (** val fieldlist_jmdiscr : fieldlist -> fieldlist -> __ **)
339 let fieldlist_jmdiscr x y =
340 Logic.eq_rect_Type2 x
342 | Fnil -> Obj.magic (fun _ dH -> dH)
343 | Fcons (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
345 type unary_operation =
350 (** val unary_operation_rect_Type4 :
351 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
352 let rec unary_operation_rect_Type4 h_Onotbool h_Onotint h_Oneg = function
353 | Onotbool -> h_Onotbool
354 | Onotint -> h_Onotint
357 (** val unary_operation_rect_Type5 :
358 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
359 let rec unary_operation_rect_Type5 h_Onotbool h_Onotint h_Oneg = function
360 | Onotbool -> h_Onotbool
361 | Onotint -> h_Onotint
364 (** val unary_operation_rect_Type3 :
365 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
366 let rec unary_operation_rect_Type3 h_Onotbool h_Onotint h_Oneg = function
367 | Onotbool -> h_Onotbool
368 | Onotint -> h_Onotint
371 (** val unary_operation_rect_Type2 :
372 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
373 let rec unary_operation_rect_Type2 h_Onotbool h_Onotint h_Oneg = function
374 | Onotbool -> h_Onotbool
375 | Onotint -> h_Onotint
378 (** val unary_operation_rect_Type1 :
379 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
380 let rec unary_operation_rect_Type1 h_Onotbool h_Onotint h_Oneg = function
381 | Onotbool -> h_Onotbool
382 | Onotint -> h_Onotint
385 (** val unary_operation_rect_Type0 :
386 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1 **)
387 let rec unary_operation_rect_Type0 h_Onotbool h_Onotint h_Oneg = function
388 | Onotbool -> h_Onotbool
389 | Onotint -> h_Onotint
392 (** val unary_operation_inv_rect_Type4 :
393 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
394 let unary_operation_inv_rect_Type4 hterm h1 h2 h3 =
395 let hcut = unary_operation_rect_Type4 h1 h2 h3 hterm in hcut __
397 (** val unary_operation_inv_rect_Type3 :
398 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
399 let unary_operation_inv_rect_Type3 hterm h1 h2 h3 =
400 let hcut = unary_operation_rect_Type3 h1 h2 h3 hterm in hcut __
402 (** val unary_operation_inv_rect_Type2 :
403 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
404 let unary_operation_inv_rect_Type2 hterm h1 h2 h3 =
405 let hcut = unary_operation_rect_Type2 h1 h2 h3 hterm in hcut __
407 (** val unary_operation_inv_rect_Type1 :
408 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
409 let unary_operation_inv_rect_Type1 hterm h1 h2 h3 =
410 let hcut = unary_operation_rect_Type1 h1 h2 h3 hterm in hcut __
412 (** val unary_operation_inv_rect_Type0 :
413 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
414 let unary_operation_inv_rect_Type0 hterm h1 h2 h3 =
415 let hcut = unary_operation_rect_Type0 h1 h2 h3 hterm in hcut __
417 (** val unary_operation_discr : unary_operation -> unary_operation -> __ **)
418 let unary_operation_discr x y =
419 Logic.eq_rect_Type2 x
421 | Onotbool -> Obj.magic (fun _ dH -> dH)
422 | Onotint -> Obj.magic (fun _ dH -> dH)
423 | Oneg -> Obj.magic (fun _ dH -> dH)) y
425 (** val unary_operation_jmdiscr :
426 unary_operation -> unary_operation -> __ **)
427 let unary_operation_jmdiscr x y =
428 Logic.eq_rect_Type2 x
430 | Onotbool -> Obj.magic (fun _ dH -> dH)
431 | Onotint -> Obj.magic (fun _ dH -> dH)
432 | Oneg -> Obj.magic (fun _ dH -> dH)) y
434 type binary_operation =
452 (** val binary_operation_rect_Type4 :
453 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
454 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
455 let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
473 (** val binary_operation_rect_Type5 :
474 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
475 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
476 let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
494 (** val binary_operation_rect_Type3 :
495 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
496 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
497 let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
515 (** val binary_operation_rect_Type2 :
516 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
517 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
518 let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
536 (** val binary_operation_rect_Type1 :
537 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
538 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
539 let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
557 (** val binary_operation_rect_Type0 :
558 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
559 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1 **)
560 let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Omod h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oeq h_One h_Olt h_Ogt h_Ole h_Oge = function
578 (** val binary_operation_inv_rect_Type4 :
579 binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
580 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
581 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
582 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
583 let binary_operation_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
585 binary_operation_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
590 (** val binary_operation_inv_rect_Type3 :
591 binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
592 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
593 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
594 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
595 let binary_operation_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
597 binary_operation_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
602 (** val binary_operation_inv_rect_Type2 :
603 binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
604 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
605 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
606 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
607 let binary_operation_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
609 binary_operation_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
614 (** val binary_operation_inv_rect_Type1 :
615 binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
616 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
617 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
618 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
619 let binary_operation_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
621 binary_operation_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
626 (** val binary_operation_inv_rect_Type0 :
627 binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
628 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
629 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
630 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
631 let binary_operation_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 =
633 binary_operation_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
638 (** val binary_operation_discr :
639 binary_operation -> binary_operation -> __ **)
640 let binary_operation_discr x y =
641 Logic.eq_rect_Type2 x
643 | Oadd -> Obj.magic (fun _ dH -> dH)
644 | Osub -> Obj.magic (fun _ dH -> dH)
645 | Omul -> Obj.magic (fun _ dH -> dH)
646 | Odiv -> Obj.magic (fun _ dH -> dH)
647 | Omod -> Obj.magic (fun _ dH -> dH)
648 | Oand -> Obj.magic (fun _ dH -> dH)
649 | Oor -> Obj.magic (fun _ dH -> dH)
650 | Oxor -> Obj.magic (fun _ dH -> dH)
651 | Oshl -> Obj.magic (fun _ dH -> dH)
652 | Oshr -> Obj.magic (fun _ dH -> dH)
653 | Oeq -> Obj.magic (fun _ dH -> dH)
654 | One -> Obj.magic (fun _ dH -> dH)
655 | Olt -> Obj.magic (fun _ dH -> dH)
656 | Ogt -> Obj.magic (fun _ dH -> dH)
657 | Ole -> Obj.magic (fun _ dH -> dH)
658 | Oge -> Obj.magic (fun _ dH -> dH)) y
660 (** val binary_operation_jmdiscr :
661 binary_operation -> binary_operation -> __ **)
662 let binary_operation_jmdiscr x y =
663 Logic.eq_rect_Type2 x
665 | Oadd -> Obj.magic (fun _ dH -> dH)
666 | Osub -> Obj.magic (fun _ dH -> dH)
667 | Omul -> Obj.magic (fun _ dH -> dH)
668 | Odiv -> Obj.magic (fun _ dH -> dH)
669 | Omod -> Obj.magic (fun _ dH -> dH)
670 | Oand -> Obj.magic (fun _ dH -> dH)
671 | Oor -> Obj.magic (fun _ dH -> dH)
672 | Oxor -> Obj.magic (fun _ dH -> dH)
673 | Oshl -> Obj.magic (fun _ dH -> dH)
674 | Oshr -> Obj.magic (fun _ dH -> dH)
675 | Oeq -> Obj.magic (fun _ dH -> dH)
676 | One -> Obj.magic (fun _ dH -> dH)
677 | Olt -> Obj.magic (fun _ dH -> dH)
678 | Ogt -> Obj.magic (fun _ dH -> dH)
679 | Ole -> Obj.magic (fun _ dH -> dH)
680 | Oge -> Obj.magic (fun _ dH -> dH)) y
683 | Expr of expr_descr * type0
685 | Econst_int of AST.intsize * AST.bvint
689 | Eunop of unary_operation * expr
690 | Ebinop of binary_operation * expr * expr
691 | Ecast of type0 * expr
692 | Econdition of expr * expr * expr
693 | Eandbool of expr * expr
694 | Eorbool of expr * expr
696 | Efield of expr * AST.ident
697 | Ecost of CostLabel.costlabel * expr
699 (** val expr_inv_rect_Type4 :
700 expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
701 let expr_inv_rect_Type4 hterm h1 =
702 let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
704 (** val expr_inv_rect_Type3 :
705 expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
706 let expr_inv_rect_Type3 hterm h1 =
707 let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
709 (** val expr_inv_rect_Type2 :
710 expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
711 let expr_inv_rect_Type2 hterm h1 =
712 let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
714 (** val expr_inv_rect_Type1 :
715 expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
716 let expr_inv_rect_Type1 hterm h1 =
717 let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
719 (** val expr_inv_rect_Type0 :
720 expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1 **)
721 let expr_inv_rect_Type0 hterm h1 =
722 let hcut = let Expr (x, x0) = hterm in h1 x x0 in hcut __
724 (** val expr_descr_inv_rect_Type4 :
725 expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
726 -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
727 -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
728 -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
729 (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
730 __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
731 expr -> __ -> 'a1) -> 'a1 **)
732 let expr_descr_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
735 | Econst_int (x, x0) -> h1 x x0
739 | Eunop (x, x0) -> h5 x x0
740 | Ebinop (x, x0, x1) -> h6 x x0 x1
741 | Ecast (x, x0) -> h7 x x0
742 | Econdition (x, x0, x1) -> h8 x x0 x1
743 | Eandbool (x, x0) -> h9 x x0
744 | Eorbool (x, x0) -> h10 x x0
746 | Efield (x, x0) -> h12 x x0
747 | Ecost (x, x0) -> h13 x x0
751 (** val expr_descr_inv_rect_Type3 :
752 expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
753 -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
754 -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
755 -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
756 (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
757 __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
758 expr -> __ -> 'a1) -> 'a1 **)
759 let expr_descr_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
762 | Econst_int (x, x0) -> h1 x x0
766 | Eunop (x, x0) -> h5 x x0
767 | Ebinop (x, x0, x1) -> h6 x x0 x1
768 | Ecast (x, x0) -> h7 x x0
769 | Econdition (x, x0, x1) -> h8 x x0 x1
770 | Eandbool (x, x0) -> h9 x x0
771 | Eorbool (x, x0) -> h10 x x0
773 | Efield (x, x0) -> h12 x x0
774 | Ecost (x, x0) -> h13 x x0
778 (** val expr_descr_inv_rect_Type2 :
779 expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
780 -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
781 -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
782 -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
783 (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
784 __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
785 expr -> __ -> 'a1) -> 'a1 **)
786 let expr_descr_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
789 | Econst_int (x, x0) -> h1 x x0
793 | Eunop (x, x0) -> h5 x x0
794 | Ebinop (x, x0, x1) -> h6 x x0 x1
795 | Ecast (x, x0) -> h7 x x0
796 | Econdition (x, x0, x1) -> h8 x x0 x1
797 | Eandbool (x, x0) -> h9 x x0
798 | Eorbool (x, x0) -> h10 x x0
800 | Efield (x, x0) -> h12 x x0
801 | Ecost (x, x0) -> h13 x x0
805 (** val expr_descr_inv_rect_Type1 :
806 expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
807 -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
808 -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
809 -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
810 (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
811 __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
812 expr -> __ -> 'a1) -> 'a1 **)
813 let expr_descr_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
816 | Econst_int (x, x0) -> h1 x x0
820 | Eunop (x, x0) -> h5 x x0
821 | Ebinop (x, x0, x1) -> h6 x x0 x1
822 | Ecast (x, x0) -> h7 x x0
823 | Econdition (x, x0, x1) -> h8 x x0 x1
824 | Eandbool (x, x0) -> h9 x x0
825 | Eorbool (x, x0) -> h10 x x0
827 | Efield (x, x0) -> h12 x x0
828 | Ecost (x, x0) -> h13 x x0
832 (** val expr_descr_inv_rect_Type0 :
833 expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
834 -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
835 -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1)
836 -> (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
837 (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 ->
838 __ -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel ->
839 expr -> __ -> 'a1) -> 'a1 **)
840 let expr_descr_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
843 | Econst_int (x, x0) -> h1 x x0
847 | Eunop (x, x0) -> h5 x x0
848 | Ebinop (x, x0, x1) -> h6 x x0 x1
849 | Ecast (x, x0) -> h7 x x0
850 | Econdition (x, x0, x1) -> h8 x x0 x1
851 | Eandbool (x, x0) -> h9 x x0
852 | Eorbool (x, x0) -> h10 x x0
854 | Efield (x, x0) -> h12 x x0
855 | Ecost (x, x0) -> h13 x x0
859 (** val expr_discr : expr -> expr -> __ **)
861 Logic.eq_rect_Type2 x
862 (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
864 (** val expr_descr_discr : expr_descr -> expr_descr -> __ **)
865 let expr_descr_discr x y =
866 Logic.eq_rect_Type2 x
868 | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
869 | Evar a0 -> Obj.magic (fun _ dH -> dH __)
870 | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
871 | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
872 | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
873 | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
874 | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
875 | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
876 | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
877 | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
878 | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
879 | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
880 | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
882 (** val expr_jmdiscr : expr -> expr -> __ **)
883 let expr_jmdiscr x y =
884 Logic.eq_rect_Type2 x
885 (let Expr (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
887 (** val expr_descr_jmdiscr : expr_descr -> expr_descr -> __ **)
888 let expr_descr_jmdiscr x y =
889 Logic.eq_rect_Type2 x
891 | Econst_int (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
892 | Evar a0 -> Obj.magic (fun _ dH -> dH __)
893 | Ederef a0 -> Obj.magic (fun _ dH -> dH __)
894 | Eaddrof a0 -> Obj.magic (fun _ dH -> dH __)
895 | Eunop (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
896 | Ebinop (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
897 | Ecast (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
898 | Econdition (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
899 | Eandbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
900 | Eorbool (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
901 | Esizeof a0 -> Obj.magic (fun _ dH -> dH __)
902 | Efield (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
903 | Ecost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
905 (** val typeof : expr -> type0 **)
906 let typeof = function
907 | Expr (de, te) -> te
909 type label = AST.ident
913 | Sassign of expr * expr
914 | Scall of expr Types.option * expr * expr List.list
915 | Ssequence of statement * statement
916 | Sifthenelse of expr * statement * statement
917 | Swhile of expr * statement
918 | Sdowhile of expr * statement
919 | Sfor of statement * expr * statement * statement
922 | Sreturn of expr Types.option
923 | Sswitch of expr * labeled_statements
924 | Slabel of label * statement
926 | Scost of CostLabel.costlabel * statement
927 and labeled_statements =
928 | LSdefault of statement
929 | LScase of AST.intsize * AST.bvint * statement * labeled_statements
931 (** val statement_inv_rect_Type4 :
932 statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
933 Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
934 statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
935 -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
936 -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
937 'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
938 labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
939 (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
941 let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
945 | Sassign (x, x0) -> h2 x x0
946 | Scall (x, x0, x1) -> h3 x x0 x1
947 | Ssequence (x, x0) -> h4 x x0
948 | Sifthenelse (x, x0, x1) -> h5 x x0 x1
949 | Swhile (x, x0) -> h6 x x0
950 | Sdowhile (x, x0) -> h7 x x0
951 | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
955 | Sswitch (x, x0) -> h12 x x0
956 | Slabel (x, x0) -> h13 x x0
958 | Scost (x, x0) -> h15 x x0
962 (** val statement_inv_rect_Type3 :
963 statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
964 Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
965 statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
966 -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
967 -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
968 'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
969 labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
970 (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
972 let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
976 | Sassign (x, x0) -> h2 x x0
977 | Scall (x, x0, x1) -> h3 x x0 x1
978 | Ssequence (x, x0) -> h4 x x0
979 | Sifthenelse (x, x0, x1) -> h5 x x0 x1
980 | Swhile (x, x0) -> h6 x x0
981 | Sdowhile (x, x0) -> h7 x x0
982 | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
986 | Sswitch (x, x0) -> h12 x x0
987 | Slabel (x, x0) -> h13 x x0
989 | Scost (x, x0) -> h15 x x0
993 (** val statement_inv_rect_Type2 :
994 statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
995 Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
996 statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
997 -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
998 -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
999 'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1000 labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1001 (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1003 let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1007 | Sassign (x, x0) -> h2 x x0
1008 | Scall (x, x0, x1) -> h3 x x0 x1
1009 | Ssequence (x, x0) -> h4 x x0
1010 | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1011 | Swhile (x, x0) -> h6 x x0
1012 | Sdowhile (x, x0) -> h7 x x0
1013 | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1016 | Sreturn x -> h11 x
1017 | Sswitch (x, x0) -> h12 x x0
1018 | Slabel (x, x0) -> h13 x x0
1020 | Scost (x, x0) -> h15 x x0
1024 (** val statement_inv_rect_Type1 :
1025 statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
1026 Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
1027 statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
1028 -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
1029 -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
1030 'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1031 labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1032 (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1034 let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1038 | Sassign (x, x0) -> h2 x x0
1039 | Scall (x, x0, x1) -> h3 x x0 x1
1040 | Ssequence (x, x0) -> h4 x x0
1041 | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1042 | Swhile (x, x0) -> h6 x x0
1043 | Sdowhile (x, x0) -> h7 x x0
1044 | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1047 | Sreturn x -> h11 x
1048 | Sswitch (x, x0) -> h12 x x0
1049 | Slabel (x, x0) -> h13 x x0
1051 | Scost (x, x0) -> h15 x x0
1055 (** val statement_inv_rect_Type0 :
1056 statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
1057 Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
1058 statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1)
1059 -> (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1)
1060 -> (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ ->
1061 'a1) -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
1062 labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
1063 (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1)
1065 let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 =
1069 | Sassign (x, x0) -> h2 x x0
1070 | Scall (x, x0, x1) -> h3 x x0 x1
1071 | Ssequence (x, x0) -> h4 x x0
1072 | Sifthenelse (x, x0, x1) -> h5 x x0 x1
1073 | Swhile (x, x0) -> h6 x x0
1074 | Sdowhile (x, x0) -> h7 x x0
1075 | Sfor (x, x0, x1, x2) -> h8 x x0 x1 x2
1078 | Sreturn x -> h11 x
1079 | Sswitch (x, x0) -> h12 x x0
1080 | Slabel (x, x0) -> h13 x x0
1082 | Scost (x, x0) -> h15 x x0
1086 (** val labeled_statements_inv_rect_Type4 :
1087 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1088 AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1089 let labeled_statements_inv_rect_Type4 hterm h1 h2 =
1092 | LSdefault x -> h1 x
1093 | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1097 (** val labeled_statements_inv_rect_Type3 :
1098 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1099 AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1100 let labeled_statements_inv_rect_Type3 hterm h1 h2 =
1103 | LSdefault x -> h1 x
1104 | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1108 (** val labeled_statements_inv_rect_Type2 :
1109 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1110 AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1111 let labeled_statements_inv_rect_Type2 hterm h1 h2 =
1114 | LSdefault x -> h1 x
1115 | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1119 (** val labeled_statements_inv_rect_Type1 :
1120 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1121 AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1122 let labeled_statements_inv_rect_Type1 hterm h1 h2 =
1125 | LSdefault x -> h1 x
1126 | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1130 (** val labeled_statements_inv_rect_Type0 :
1131 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize ->
1132 AST.bvint -> statement -> labeled_statements -> __ -> 'a1) -> 'a1 **)
1133 let labeled_statements_inv_rect_Type0 hterm h1 h2 =
1136 | LSdefault x -> h1 x
1137 | LScase (x, x0, x1, x2) -> h2 x x0 x1 x2
1141 (** val statement_discr : statement -> statement -> __ **)
1142 let statement_discr x y =
1143 Logic.eq_rect_Type2 x
1145 | Sskip -> Obj.magic (fun _ dH -> dH)
1146 | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1147 | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1148 | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1149 | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1150 | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1151 | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1152 | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1153 | Sbreak -> Obj.magic (fun _ dH -> dH)
1154 | Scontinue -> Obj.magic (fun _ dH -> dH)
1155 | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
1156 | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1157 | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1158 | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
1159 | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1161 (** val labeled_statements_discr :
1162 labeled_statements -> labeled_statements -> __ **)
1163 let labeled_statements_discr x y =
1164 Logic.eq_rect_Type2 x
1166 | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
1167 | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1169 (** val statement_jmdiscr : statement -> statement -> __ **)
1170 let statement_jmdiscr x y =
1171 Logic.eq_rect_Type2 x
1173 | Sskip -> Obj.magic (fun _ dH -> dH)
1174 | Sassign (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1175 | Scall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1176 | Ssequence (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1177 | Sifthenelse (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1178 | Swhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1179 | Sdowhile (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1180 | Sfor (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1181 | Sbreak -> Obj.magic (fun _ dH -> dH)
1182 | Scontinue -> Obj.magic (fun _ dH -> dH)
1183 | Sreturn a0 -> Obj.magic (fun _ dH -> dH __)
1184 | Sswitch (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1185 | Slabel (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1186 | Sgoto a0 -> Obj.magic (fun _ dH -> dH __)
1187 | Scost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1189 (** val labeled_statements_jmdiscr :
1190 labeled_statements -> labeled_statements -> __ **)
1191 let labeled_statements_jmdiscr x y =
1192 Logic.eq_rect_Type2 x
1194 | LSdefault a0 -> Obj.magic (fun _ dH -> dH __)
1195 | LScase (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1197 type function0 = { fn_return : type0;
1198 fn_params : (AST.ident, type0) Types.prod List.list;
1199 fn_vars : (AST.ident, type0) Types.prod List.list;
1200 fn_body : statement }
1202 (** val function_rect_Type4 :
1203 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1204 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1205 let rec function_rect_Type4 h_mk_function x_4495 =
1206 let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1207 fn_body = fn_body0 } = x_4495
1209 h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1211 (** val function_rect_Type5 :
1212 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1213 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1214 let rec function_rect_Type5 h_mk_function x_4497 =
1215 let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1216 fn_body = fn_body0 } = x_4497
1218 h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1220 (** val function_rect_Type3 :
1221 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1222 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1223 let rec function_rect_Type3 h_mk_function x_4499 =
1224 let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1225 fn_body = fn_body0 } = x_4499
1227 h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1229 (** val function_rect_Type2 :
1230 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1231 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1232 let rec function_rect_Type2 h_mk_function x_4501 =
1233 let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1234 fn_body = fn_body0 } = x_4501
1236 h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1238 (** val function_rect_Type1 :
1239 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1240 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1241 let rec function_rect_Type1 h_mk_function x_4503 =
1242 let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1243 fn_body = fn_body0 } = x_4503
1245 h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1247 (** val function_rect_Type0 :
1248 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
1249 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
1250 let rec function_rect_Type0 h_mk_function x_4505 =
1251 let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
1252 fn_body = fn_body0 } = x_4505
1254 h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
1256 (** val fn_return : function0 -> type0 **)
1257 let rec fn_return xxx =
1260 (** val fn_params : function0 -> (AST.ident, type0) Types.prod List.list **)
1261 let rec fn_params xxx =
1264 (** val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list **)
1265 let rec fn_vars xxx =
1268 (** val fn_body : function0 -> statement **)
1269 let rec fn_body xxx =
1272 (** val function_inv_rect_Type4 :
1273 function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1274 (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1275 let function_inv_rect_Type4 hterm h1 =
1276 let hcut = function_rect_Type4 h1 hterm in hcut __
1278 (** val function_inv_rect_Type3 :
1279 function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1280 (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1281 let function_inv_rect_Type3 hterm h1 =
1282 let hcut = function_rect_Type3 h1 hterm in hcut __
1284 (** val function_inv_rect_Type2 :
1285 function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1286 (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1287 let function_inv_rect_Type2 hterm h1 =
1288 let hcut = function_rect_Type2 h1 hterm in hcut __
1290 (** val function_inv_rect_Type1 :
1291 function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1292 (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1293 let function_inv_rect_Type1 hterm h1 =
1294 let hcut = function_rect_Type1 h1 hterm in hcut __
1296 (** val function_inv_rect_Type0 :
1297 function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
1298 (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1 **)
1299 let function_inv_rect_Type0 hterm h1 =
1300 let hcut = function_rect_Type0 h1 hterm in hcut __
1302 (** val function_discr : function0 -> function0 -> __ **)
1303 let function_discr x y =
1304 Logic.eq_rect_Type2 x
1305 (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
1307 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1309 (** val function_jmdiscr : function0 -> function0 -> __ **)
1310 let function_jmdiscr x y =
1311 Logic.eq_rect_Type2 x
1312 (let { fn_return = a0; fn_params = a1; fn_vars = a2; fn_body = a3 } = x
1314 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1316 type clight_fundef =
1317 | CL_Internal of function0
1318 | CL_External of AST.ident * typelist * type0
1320 (** val clight_fundef_rect_Type4 :
1321 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1322 clight_fundef -> 'a1 **)
1323 let rec clight_fundef_rect_Type4 h_CL_Internal h_CL_External = function
1324 | CL_Internal x_4527 -> h_CL_Internal x_4527
1325 | CL_External (x_4530, x_4529, x_4528) -> h_CL_External x_4530 x_4529 x_4528
1327 (** val clight_fundef_rect_Type5 :
1328 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1329 clight_fundef -> 'a1 **)
1330 let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
1331 | CL_Internal x_4534 -> h_CL_Internal x_4534
1332 | CL_External (x_4537, x_4536, x_4535) -> h_CL_External x_4537 x_4536 x_4535
1334 (** val clight_fundef_rect_Type3 :
1335 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1336 clight_fundef -> 'a1 **)
1337 let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
1338 | CL_Internal x_4541 -> h_CL_Internal x_4541
1339 | CL_External (x_4544, x_4543, x_4542) -> h_CL_External x_4544 x_4543 x_4542
1341 (** val clight_fundef_rect_Type2 :
1342 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1343 clight_fundef -> 'a1 **)
1344 let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
1345 | CL_Internal x_4548 -> h_CL_Internal x_4548
1346 | CL_External (x_4551, x_4550, x_4549) -> h_CL_External x_4551 x_4550 x_4549
1348 (** val clight_fundef_rect_Type1 :
1349 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1350 clight_fundef -> 'a1 **)
1351 let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
1352 | CL_Internal x_4555 -> h_CL_Internal x_4555
1353 | CL_External (x_4558, x_4557, x_4556) -> h_CL_External x_4558 x_4557 x_4556
1355 (** val clight_fundef_rect_Type0 :
1356 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
1357 clight_fundef -> 'a1 **)
1358 let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
1359 | CL_Internal x_4562 -> h_CL_Internal x_4562
1360 | CL_External (x_4565, x_4564, x_4563) -> h_CL_External x_4565 x_4564 x_4563
1362 (** val clight_fundef_inv_rect_Type4 :
1363 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1364 type0 -> __ -> 'a1) -> 'a1 **)
1365 let clight_fundef_inv_rect_Type4 hterm h1 h2 =
1366 let hcut = clight_fundef_rect_Type4 h1 h2 hterm in hcut __
1368 (** val clight_fundef_inv_rect_Type3 :
1369 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1370 type0 -> __ -> 'a1) -> 'a1 **)
1371 let clight_fundef_inv_rect_Type3 hterm h1 h2 =
1372 let hcut = clight_fundef_rect_Type3 h1 h2 hterm in hcut __
1374 (** val clight_fundef_inv_rect_Type2 :
1375 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1376 type0 -> __ -> 'a1) -> 'a1 **)
1377 let clight_fundef_inv_rect_Type2 hterm h1 h2 =
1378 let hcut = clight_fundef_rect_Type2 h1 h2 hterm in hcut __
1380 (** val clight_fundef_inv_rect_Type1 :
1381 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1382 type0 -> __ -> 'a1) -> 'a1 **)
1383 let clight_fundef_inv_rect_Type1 hterm h1 h2 =
1384 let hcut = clight_fundef_rect_Type1 h1 h2 hterm in hcut __
1386 (** val clight_fundef_inv_rect_Type0 :
1387 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
1388 type0 -> __ -> 'a1) -> 'a1 **)
1389 let clight_fundef_inv_rect_Type0 hterm h1 h2 =
1390 let hcut = clight_fundef_rect_Type0 h1 h2 hterm in hcut __
1392 (** val clight_fundef_discr : clight_fundef -> clight_fundef -> __ **)
1393 let clight_fundef_discr x y =
1394 Logic.eq_rect_Type2 x
1396 | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1397 | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1399 (** val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __ **)
1400 let clight_fundef_jmdiscr x y =
1401 Logic.eq_rect_Type2 x
1403 | CL_Internal a0 -> Obj.magic (fun _ dH -> dH __)
1404 | CL_External (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
1406 type clight_program =
1407 (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
1409 (** val type_of_params :
1410 (AST.ident, type0) Types.prod List.list -> typelist **)
1411 let rec type_of_params = function
1413 | List.Cons (h, rem) ->
1414 let { Types.fst = id; Types.snd = ty } = h in
1415 Tcons (ty, (type_of_params rem))
1417 (** val type_of_function : function0 -> type0 **)
1418 let type_of_function f =
1419 Tfunction ((type_of_params f.fn_params), f.fn_return)
1421 (** val type_of_fundef : clight_fundef -> type0 **)
1422 let type_of_fundef = function
1423 | CL_Internal fd -> type_of_function fd
1424 | CL_External (id, args, res) -> Tfunction (args, res)
1426 (** val alignof : type0 -> Nat.nat **)
1427 let rec alignof = function
1428 | Tvoid -> Nat.S Nat.O
1431 | AST.I8 -> Nat.S Nat.O
1432 | AST.I16 -> Nat.S (Nat.S Nat.O)
1433 | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1434 | Tpointer x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1435 | Tarray (t', n) -> alignof t'
1436 | Tfunction (x, x0) -> Nat.S Nat.O
1437 | Tstruct (x, fld) -> alignof_fields fld
1438 | Tunion (x, fld) -> alignof_fields fld
1439 | Tcomp_ptr x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
1440 (** val alignof_fields : fieldlist -> Nat.nat **)
1441 and alignof_fields = function
1442 | Fnil -> Nat.S Nat.O
1443 | Fcons (id, t, f') -> Nat.max (alignof t) (alignof_fields f')
1445 (** val sizeof : type0 -> Nat.nat **)
1446 let rec sizeof t = match t with
1447 | Tvoid -> Nat.S Nat.O
1450 | AST.I8 -> Nat.S Nat.O
1451 | AST.I16 -> Nat.S (Nat.S Nat.O)
1452 | AST.I32 -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
1453 | Tpointer x -> AST.size_pointer
1454 | Tarray (t', n) -> Nat.times (sizeof t') (Nat.max (Nat.S Nat.O) n)
1455 | Tfunction (x, x0) -> Nat.S Nat.O
1456 | Tstruct (x, fld) ->
1457 Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_struct fld Nat.O)) (alignof t)
1458 | Tunion (x, fld) ->
1459 Coqlib.align (Nat.max (Nat.S Nat.O) (sizeof_union fld)) (alignof t)
1460 | Tcomp_ptr x -> AST.size_pointer
1461 (** val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat **)
1462 and sizeof_struct fld pos =
1465 | Fcons (id, t, fld') ->
1466 sizeof_struct fld' (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t))
1467 (** val sizeof_union : fieldlist -> Nat.nat **)
1468 and sizeof_union = function
1470 | Fcons (id, t, fld') -> Nat.max (sizeof t) (sizeof_union fld')
1472 (** val field_offset_rec :
1473 AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res **)
1474 let rec field_offset_rec id fld pos =
1477 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1478 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1479 | Fcons (id', t, fld') ->
1480 (match AST.ident_eq id id' with
1481 | Types.Inl _ -> Errors.OK (Coqlib.align pos (alignof t))
1483 field_offset_rec id fld'
1484 (Nat.plus (Coqlib.align pos (alignof t)) (sizeof t)))
1486 (** val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res **)
1487 let field_offset id fld =
1488 field_offset_rec id fld Nat.O
1490 (** val field_type : AST.ident -> fieldlist -> type0 Errors.res **)
1491 let rec field_type id = function
1493 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
1494 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
1495 | Fcons (id', t, fld') ->
1496 (match AST.ident_eq id id' with
1497 | Types.Inl _ -> Errors.OK t
1498 | Types.Inr _ -> field_type id fld')
1500 (** val typ_of_type : type0 -> AST.typ **)
1501 let typ_of_type = function
1502 | Tvoid -> AST.ASTint (AST.I32, AST.Unsigned)
1503 | Tint (sz, sg) -> AST.ASTint (sz, sg)
1504 | Tpointer x -> AST.ASTptr
1505 | Tarray (x, x0) -> AST.ASTptr
1506 | Tfunction (x, x0) -> AST.ASTptr
1507 | Tstruct (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1508 | Tunion (x, x0) -> AST.ASTint (AST.I32, AST.Unsigned)
1509 | Tcomp_ptr x -> AST.ASTptr
1511 (** val opttyp_of_type : type0 -> AST.typ Types.option **)
1512 let opttyp_of_type = function
1513 | Tvoid -> Types.None
1514 | Tint (sz, sg) -> Types.Some (AST.ASTint (sz, sg))
1515 | Tpointer x -> Types.Some AST.ASTptr
1516 | Tarray (x, x0) -> Types.Some AST.ASTptr
1517 | Tfunction (x, x0) -> Types.Some AST.ASTptr
1518 | Tstruct (x, x0) -> Types.None
1519 | Tunion (x, x0) -> Types.None
1520 | Tcomp_ptr x -> Types.Some AST.ASTptr
1522 (** val typlist_of_typelist : typelist -> AST.typ List.list **)
1523 let rec typlist_of_typelist = function
1525 | Tcons (hd, tl0) -> List.Cons ((typ_of_type hd), (typlist_of_typelist tl0))
1528 | By_value of AST.typ
1530 | By_nothing of AST.typ
1532 (** val mode_rect_Type4 :
1533 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1534 let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4615 = function
1535 | By_value t -> h_By_value t
1536 | By_reference -> h_By_reference
1537 | By_nothing t -> h_By_nothing t
1539 (** val mode_rect_Type5 :
1540 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1541 let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4620 = function
1542 | By_value t -> h_By_value t
1543 | By_reference -> h_By_reference
1544 | By_nothing t -> h_By_nothing t
1546 (** val mode_rect_Type3 :
1547 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1548 let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4625 = function
1549 | By_value t -> h_By_value t
1550 | By_reference -> h_By_reference
1551 | By_nothing t -> h_By_nothing t
1553 (** val mode_rect_Type2 :
1554 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1555 let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4630 = function
1556 | By_value t -> h_By_value t
1557 | By_reference -> h_By_reference
1558 | By_nothing t -> h_By_nothing t
1560 (** val mode_rect_Type1 :
1561 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1562 let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4635 = function
1563 | By_value t -> h_By_value t
1564 | By_reference -> h_By_reference
1565 | By_nothing t -> h_By_nothing t
1567 (** val mode_rect_Type0 :
1568 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
1569 let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4640 = function
1570 | By_value t -> h_By_value t
1571 | By_reference -> h_By_reference
1572 | By_nothing t -> h_By_nothing t
1574 (** val mode_inv_rect_Type4 :
1575 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1576 (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1577 let mode_inv_rect_Type4 x1 hterm h1 h2 h3 =
1578 let hcut = mode_rect_Type4 h1 h2 h3 x1 hterm in hcut __ __
1580 (** val mode_inv_rect_Type3 :
1581 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1582 (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1583 let mode_inv_rect_Type3 x1 hterm h1 h2 h3 =
1584 let hcut = mode_rect_Type3 h1 h2 h3 x1 hterm in hcut __ __
1586 (** val mode_inv_rect_Type2 :
1587 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1588 (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1589 let mode_inv_rect_Type2 x1 hterm h1 h2 h3 =
1590 let hcut = mode_rect_Type2 h1 h2 h3 x1 hterm in hcut __ __
1592 (** val mode_inv_rect_Type1 :
1593 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1594 (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1595 let mode_inv_rect_Type1 x1 hterm h1 h2 h3 =
1596 let hcut = mode_rect_Type1 h1 h2 h3 x1 hterm in hcut __ __
1598 (** val mode_inv_rect_Type0 :
1599 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
1600 (AST.typ -> __ -> __ -> 'a1) -> 'a1 **)
1601 let mode_inv_rect_Type0 x1 hterm h1 h2 h3 =
1602 let hcut = mode_rect_Type0 h1 h2 h3 x1 hterm in hcut __ __
1604 (** val mode_discr : AST.typ -> mode -> mode -> __ **)
1605 let mode_discr a1 x y =
1606 Logic.eq_rect_Type2 x
1608 | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1609 | By_reference -> Obj.magic (fun _ dH -> dH)
1610 | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1612 (** val mode_jmdiscr : AST.typ -> mode -> mode -> __ **)
1613 let mode_jmdiscr a1 x y =
1614 Logic.eq_rect_Type2 x
1616 | By_value a0 -> Obj.magic (fun _ dH -> dH __)
1617 | By_reference -> Obj.magic (fun _ dH -> dH)
1618 | By_nothing a0 -> Obj.magic (fun _ dH -> dH __)) y
1620 (** val access_mode : type0 -> mode **)
1621 let access_mode = function
1622 | Tvoid -> By_nothing (typ_of_type Tvoid)
1623 | Tint (i, s) -> By_value (AST.ASTint (i, s))
1624 | Tpointer x -> By_value AST.ASTptr
1625 | Tarray (x, x0) -> By_reference
1626 | Tfunction (x, x0) -> By_reference
1627 | Tstruct (x, fList) -> By_nothing (typ_of_type (Tstruct (x, fList)))
1628 | Tunion (x, fList) -> By_nothing (typ_of_type (Tunion (x, fList)))
1629 | Tcomp_ptr x -> By_value AST.ASTptr
1631 (** val signature_of_type : typelist -> type0 -> AST.signature **)
1632 let signature_of_type args res =
1633 { AST.sig_args = (typlist_of_typelist args); AST.sig_res =
1634 (opttyp_of_type res) }
1636 (** val external_function :
1637 AST.ident -> typelist -> type0 -> AST.external_function **)
1638 let external_function id targs tres =
1639 { AST.ef_id = id; AST.ef_sig = (signature_of_type targs tres) }