41 open Hints_declaration
79 (* singleton inductive, whose constructor was mk_block *)
81 (** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
82 let rec block_rect_Type4 h_mk_block x_5028 =
83 let block_id = x_5028 in h_mk_block block_id
85 (** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
86 let rec block_rect_Type5 h_mk_block x_5030 =
87 let block_id = x_5030 in h_mk_block block_id
89 (** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
90 let rec block_rect_Type3 h_mk_block x_5032 =
91 let block_id = x_5032 in h_mk_block block_id
93 (** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
94 let rec block_rect_Type2 h_mk_block x_5034 =
95 let block_id = x_5034 in h_mk_block block_id
97 (** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
98 let rec block_rect_Type1 h_mk_block x_5036 =
99 let block_id = x_5036 in h_mk_block block_id
101 (** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
102 let rec block_rect_Type0 h_mk_block x_5038 =
103 let block_id = x_5038 in h_mk_block block_id
105 (** val block_id : block -> Z.z **)
106 let rec block_id xxx =
109 (** val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
110 let block_inv_rect_Type4 hterm h1 =
111 let hcut = block_rect_Type4 h1 hterm in hcut __
113 (** val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
114 let block_inv_rect_Type3 hterm h1 =
115 let hcut = block_rect_Type3 h1 hterm in hcut __
117 (** val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
118 let block_inv_rect_Type2 hterm h1 =
119 let hcut = block_rect_Type2 h1 hterm in hcut __
121 (** val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
122 let block_inv_rect_Type1 hterm h1 =
123 let hcut = block_rect_Type1 h1 hterm in hcut __
125 (** val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
126 let block_inv_rect_Type0 hterm h1 =
127 let hcut = block_rect_Type0 h1 hterm in hcut __
129 (** val block_discr : block -> block -> __ **)
130 let block_discr x y =
131 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
133 (** val block_jmdiscr : block -> block -> __ **)
134 let block_jmdiscr x y =
135 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
137 (** val block_region : block -> AST.region **)
139 match Z.zleb (block_id b) Z.OZ with
140 | Bool.True -> AST.Code
141 | Bool.False -> AST.XData
143 (** val dummy_block_code : block **)
144 let dummy_block_code =
147 (** val eq_block : block -> block -> Bool.bool **)
149 Z.eqZb (block_id b1) (block_id b2)
151 (** val block_eq : Deqsets.deqSet **)
155 (** val offset_size : Nat.nat **)
157 Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
158 Nat.O)))))))) AST.size_pointer
162 (* singleton inductive, whose constructor was mk_offset *)
164 (** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
165 let rec offset_rect_Type4 h_mk_offset x_5054 =
166 let offv = x_5054 in h_mk_offset offv
168 (** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
169 let rec offset_rect_Type5 h_mk_offset x_5056 =
170 let offv = x_5056 in h_mk_offset offv
172 (** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
173 let rec offset_rect_Type3 h_mk_offset x_5058 =
174 let offv = x_5058 in h_mk_offset offv
176 (** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
177 let rec offset_rect_Type2 h_mk_offset x_5060 =
178 let offv = x_5060 in h_mk_offset offv
180 (** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
181 let rec offset_rect_Type1 h_mk_offset x_5062 =
182 let offv = x_5062 in h_mk_offset offv
184 (** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
185 let rec offset_rect_Type0 h_mk_offset x_5064 =
186 let offv = x_5064 in h_mk_offset offv
188 (** val offv : offset -> BitVector.bitVector **)
192 (** val offset_inv_rect_Type4 :
193 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
194 let offset_inv_rect_Type4 hterm h1 =
195 let hcut = offset_rect_Type4 h1 hterm in hcut __
197 (** val offset_inv_rect_Type3 :
198 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
199 let offset_inv_rect_Type3 hterm h1 =
200 let hcut = offset_rect_Type3 h1 hterm in hcut __
202 (** val offset_inv_rect_Type2 :
203 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
204 let offset_inv_rect_Type2 hterm h1 =
205 let hcut = offset_rect_Type2 h1 hterm in hcut __
207 (** val offset_inv_rect_Type1 :
208 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
209 let offset_inv_rect_Type1 hterm h1 =
210 let hcut = offset_rect_Type1 h1 hterm in hcut __
212 (** val offset_inv_rect_Type0 :
213 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
214 let offset_inv_rect_Type0 hterm h1 =
215 let hcut = offset_rect_Type0 h1 hterm in hcut __
217 (** val offset_discr : offset -> offset -> __ **)
218 let offset_discr x y =
219 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
221 (** val offset_jmdiscr : offset -> offset -> __ **)
222 let offset_jmdiscr x y =
223 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
225 (** val eq_offset : offset -> offset -> Bool.bool **)
227 BitVector.eq_bv offset_size (offv x) (offv y)
229 (** val offset_of_Z : Z.z -> offset **)
231 BitVectorZ.bitvector_of_Z offset_size z
233 (** val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset **)
234 let shift_offset n o i =
235 Arithmetic.addition_n offset_size (offv o)
236 (Arithmetic.sign_ext n offset_size i)
238 (** val shift_offset_n :
239 Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
241 let shift_offset_n n o i sg j =
242 Arithmetic.addition_n offset_size (offv o)
243 (Arithmetic.short_multiplication offset_size
244 (Arithmetic.bitvector_of_nat offset_size i)
246 | AST.Signed -> Arithmetic.sign_ext n offset_size j
247 | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
249 (** val neg_shift_offset :
250 Nat.nat -> offset -> BitVector.bitVector -> offset **)
251 let neg_shift_offset n o i =
252 Arithmetic.subtraction offset_size (offv o)
253 (Arithmetic.sign_ext n offset_size i)
255 (** val neg_shift_offset_n :
256 Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
258 let neg_shift_offset_n n o i sg j =
259 Arithmetic.subtraction offset_size (offv o)
260 (Arithmetic.short_multiplication offset_size
261 (Arithmetic.bitvector_of_nat offset_size i)
263 | AST.Signed -> Arithmetic.sign_ext n offset_size j
264 | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
266 (** val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector **)
267 let sub_offset n x y =
268 Arithmetic.sign_ext offset_size n
269 (Arithmetic.subtraction offset_size (offv x) (offv y))
271 (** val zero_offset : offset **)
273 BitVector.zero offset_size
275 (** val lt_offset : offset -> offset -> Bool.bool **)
277 Arithmetic.lt_u offset_size (offv x) (offv y)
279 type pointer = { pblock : block; poff : offset }
281 (** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
282 let rec pointer_rect_Type4 h_mk_pointer x_5080 =
283 let { pblock = pblock0; poff = poff0 } = x_5080 in
284 h_mk_pointer pblock0 poff0
286 (** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
287 let rec pointer_rect_Type5 h_mk_pointer x_5082 =
288 let { pblock = pblock0; poff = poff0 } = x_5082 in
289 h_mk_pointer pblock0 poff0
291 (** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
292 let rec pointer_rect_Type3 h_mk_pointer x_5084 =
293 let { pblock = pblock0; poff = poff0 } = x_5084 in
294 h_mk_pointer pblock0 poff0
296 (** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
297 let rec pointer_rect_Type2 h_mk_pointer x_5086 =
298 let { pblock = pblock0; poff = poff0 } = x_5086 in
299 h_mk_pointer pblock0 poff0
301 (** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
302 let rec pointer_rect_Type1 h_mk_pointer x_5088 =
303 let { pblock = pblock0; poff = poff0 } = x_5088 in
304 h_mk_pointer pblock0 poff0
306 (** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
307 let rec pointer_rect_Type0 h_mk_pointer x_5090 =
308 let { pblock = pblock0; poff = poff0 } = x_5090 in
309 h_mk_pointer pblock0 poff0
311 (** val pblock : pointer -> block **)
315 (** val poff : pointer -> offset **)
319 (** val pointer_inv_rect_Type4 :
320 pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
321 let pointer_inv_rect_Type4 hterm h1 =
322 let hcut = pointer_rect_Type4 h1 hterm in hcut __
324 (** val pointer_inv_rect_Type3 :
325 pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
326 let pointer_inv_rect_Type3 hterm h1 =
327 let hcut = pointer_rect_Type3 h1 hterm in hcut __
329 (** val pointer_inv_rect_Type2 :
330 pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
331 let pointer_inv_rect_Type2 hterm h1 =
332 let hcut = pointer_rect_Type2 h1 hterm in hcut __
334 (** val pointer_inv_rect_Type1 :
335 pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
336 let pointer_inv_rect_Type1 hterm h1 =
337 let hcut = pointer_rect_Type1 h1 hterm in hcut __
339 (** val pointer_inv_rect_Type0 :
340 pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
341 let pointer_inv_rect_Type0 hterm h1 =
342 let hcut = pointer_rect_Type0 h1 hterm in hcut __
344 (** val pointer_discr : pointer -> pointer -> __ **)
345 let pointer_discr x y =
346 Logic.eq_rect_Type2 x
347 (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
350 (** val pointer_jmdiscr : pointer -> pointer -> __ **)
351 let pointer_jmdiscr x y =
352 Logic.eq_rect_Type2 x
353 (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
356 (** val ptype : pointer -> AST.region **)
358 block_region p.pblock
360 (** val shift_pointer :
361 Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
362 let shift_pointer n p i =
363 { pblock = p.pblock; poff = (shift_offset n p.poff i) }
365 (** val shift_pointer_n :
366 Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
368 let shift_pointer_n n p i sg j =
369 { pblock = p.pblock; poff = (shift_offset_n n p.poff i sg j) }
371 (** val neg_shift_pointer :
372 Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
373 let neg_shift_pointer n p i =
374 { pblock = p.pblock; poff = (neg_shift_offset n p.poff i) }
376 (** val neg_shift_pointer_n :
377 Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
379 let neg_shift_pointer_n n p i sg j =
380 { pblock = p.pblock; poff = (neg_shift_offset_n n p.poff i sg j) }
382 (** val eq_pointer : pointer -> pointer -> Bool.bool **)
383 let eq_pointer p1 p2 =
384 Bool.andb (eq_block p1.pblock p2.pblock) (eq_offset p1.poff p2.poff)