41 open Hints_declaration
79 (* singleton inductive, whose constructor was mk_block *)
81 val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1
83 val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1
85 val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1
87 val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1
89 val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1
91 val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1
93 val block_id : block -> Z.z
95 val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1
97 val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1
99 val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1
101 val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1
103 val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1
105 val block_discr : block -> block -> __
107 val block_jmdiscr : block -> block -> __
109 val block_region : block -> AST.region
111 val dummy_block_code : block
113 val eq_block : block -> block -> Bool.bool
115 val block_eq : Deqsets.deqSet
117 val offset_size : Nat.nat
121 (* singleton inductive, whose constructor was mk_offset *)
123 val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
125 val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
127 val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
129 val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
131 val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
133 val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1
135 val offv : offset -> BitVector.bitVector
137 val offset_inv_rect_Type4 :
138 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
140 val offset_inv_rect_Type3 :
141 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
143 val offset_inv_rect_Type2 :
144 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
146 val offset_inv_rect_Type1 :
147 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
149 val offset_inv_rect_Type0 :
150 offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1
152 val offset_discr : offset -> offset -> __
154 val offset_jmdiscr : offset -> offset -> __
156 val eq_offset : offset -> offset -> Bool.bool
158 val offset_of_Z : Z.z -> offset
160 val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
163 Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
166 val neg_shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset
168 val neg_shift_offset_n :
169 Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
172 val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector
174 val zero_offset : offset
176 val lt_offset : offset -> offset -> Bool.bool
178 type pointer = { pblock : block; poff : offset }
180 val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1
182 val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1
184 val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1
186 val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1
188 val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1
190 val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1
192 val pblock : pointer -> block
194 val poff : pointer -> offset
196 val pointer_inv_rect_Type4 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
198 val pointer_inv_rect_Type3 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
200 val pointer_inv_rect_Type2 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
202 val pointer_inv_rect_Type1 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
204 val pointer_inv_rect_Type0 : pointer -> (block -> offset -> __ -> 'a1) -> 'a1
206 val pointer_discr : pointer -> pointer -> __
208 val pointer_jmdiscr : pointer -> pointer -> __
210 val ptype : pointer -> AST.region
212 val shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
214 val shift_pointer_n :
215 Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
218 val neg_shift_pointer : Nat.nat -> pointer -> BitVector.bitVector -> pointer
220 val neg_shift_pointer_n :
221 Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
224 val eq_pointer : pointer -> pointer -> Bool.bool