97 open Hints_declaration
139 val size_of_sig_type : AST.typ -> Nat.nat
141 val sign_of_sig_type : AST.typ -> AST.signedness
144 | Register_int of Registers.register
145 | Register_ptr of Registers.register * Registers.register
147 val register_type_rect_Type4 :
148 (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
149 'a1) -> register_type -> 'a1
151 val register_type_rect_Type5 :
152 (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
153 'a1) -> register_type -> 'a1
155 val register_type_rect_Type3 :
156 (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
157 'a1) -> register_type -> 'a1
159 val register_type_rect_Type2 :
160 (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
161 'a1) -> register_type -> 'a1
163 val register_type_rect_Type1 :
164 (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
165 'a1) -> register_type -> 'a1
167 val register_type_rect_Type0 :
168 (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
169 'a1) -> register_type -> 'a1
171 val register_type_inv_rect_Type4 :
172 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
173 -> Registers.register -> __ -> 'a1) -> 'a1
175 val register_type_inv_rect_Type3 :
176 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
177 -> Registers.register -> __ -> 'a1) -> 'a1
179 val register_type_inv_rect_Type2 :
180 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
181 -> Registers.register -> __ -> 'a1) -> 'a1
183 val register_type_inv_rect_Type1 :
184 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
185 -> Registers.register -> __ -> 'a1) -> 'a1
187 val register_type_inv_rect_Type0 :
188 register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
189 -> Registers.register -> __ -> 'a1) -> 'a1
191 val register_type_discr : register_type -> register_type -> __
193 val register_type_jmdiscr : register_type -> register_type -> __
195 type local_env = Registers.register List.list Identifiers.identifier_map
198 PreIdentifiers.identifier -> local_env -> Registers.register List.list
200 val find_local_env_arg :
201 Registers.register -> local_env -> Joint.psd_argument List.list
203 val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __
205 val fresh_registers :
206 Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
207 List.list Monad.smax_def__o__monad
209 val map_list_local_env :
210 Registers.register List.list Identifiers.identifier_map ->
211 (Registers.register, AST.typ) Types.prod List.list -> Registers.register
214 val initialize_local_env :
215 AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
216 -> local_env Monad.smax_def__o__monad
218 val initialize_locals_params_ret :
219 AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
220 -> (Registers.register, AST.typ) Types.prod List.list ->
221 (Registers.register, AST.typ) Types.prod Types.option -> local_env
222 Monad.smax_def__o__monad
224 val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod
227 PreIdentifiers.identifier -> local_env -> (Registers.register,
228 Registers.register) Types.prod
230 val find_and_addr_arg :
231 Registers.register -> local_env -> (Joint.psd_argument, Joint.psd_argument)
235 Registers.register List.list -> local_env -> Joint.psd_argument List.list
238 Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
241 val split_into_bytes :
242 AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0
244 val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
246 val translate_op_aux :
247 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
248 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
249 Joint.joint_seq List.list
252 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
253 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
254 Joint.joint_seq List.list
256 val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list
258 val translate_op_asym_unsigned :
259 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
260 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
261 Joint.joint_seq List.list
263 val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
265 val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
267 val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat
270 AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
271 Registers.register List.list -> (Registers.register, Joint.joint_seq
272 List.list) Bind_new.bind_new
275 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
276 List.list -> Joint.joint_seq List.list
279 AST.ident List.list -> Registers.register -> Joint.psd_argument ->
280 Joint.joint_seq List.list
282 val translate_cast_signed :
283 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
284 -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
286 val translate_fill_with_zero :
287 AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
290 val last : 'a1 List.list -> 'a1 Types.option
292 val translate_op_asym_signed :
293 AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
294 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
295 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
298 AST.ident List.list -> AST.signedness -> Registers.register List.list ->
299 Registers.register List.list -> (Registers.register, Joint.joint_seq
300 List.list) Bind_new.bind_new
302 val translate_notint :
303 AST.ident List.list -> Registers.register List.list -> Registers.register
304 List.list -> Joint.joint_seq List.list
306 val translate_negint :
307 AST.ident List.list -> Registers.register List.list -> Registers.register
308 List.list -> Joint.joint_seq List.list
310 val translate_notbool :
311 AST.ident List.list -> Registers.register List.list -> Registers.register
312 List.list -> (Registers.register, Joint.joint_seq List.list)
316 AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
317 Registers.register List.list -> Registers.register List.list ->
318 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
320 val translate_mul_i :
321 AST.ident List.list -> Registers.register -> Registers.register -> Nat.nat
322 -> Registers.register List.list -> Joint.psd_argument List.list ->
323 Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
324 Joint.joint_seq List.list -> Joint.joint_seq List.list
327 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
328 List.list -> Joint.psd_argument List.list -> (Registers.register,
329 Joint.joint_seq List.list) Bind_new.bind_new
331 val translate_divumodu8 :
332 AST.ident List.list -> Bool.bool -> Registers.register List.list ->
333 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
334 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
337 ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list -> 'a3
340 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
341 List.list -> Joint.psd_argument List.list -> (Registers.register,
342 Joint.joint_seq List.list) Bind_new.bind_new
344 val translate_toggle_bool :
345 AST.ident List.list -> Registers.register List.list -> (Registers.register,
346 Joint.joint_seq List.list) Bind_new.bind_new
348 val translate_lt_unsigned :
349 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
350 List.list -> Joint.psd_argument List.list -> (Registers.register,
351 Joint.joint_seq List.list) Bind_new.bind_new
354 AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
355 -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
358 val translate_lt_signed :
359 AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
360 List.list -> Joint.psd_argument List.list -> (Registers.register,
361 Joint.joint_seq List.list) Bind_new.bind_new
364 Bool.bool -> AST.ident List.list -> Registers.register List.list ->
365 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
366 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
369 Bool.bool -> AST.ident List.list -> Integers.comparison ->
370 Registers.register List.list -> Joint.psd_argument List.list ->
371 Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
375 AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
376 FrontEndOps.binary_operation -> Registers.register List.list ->
377 Joint.psd_argument List.list -> Joint.psd_argument List.list ->
378 (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
381 AST.ident List.list -> Registers.register List.list -> Graphs.label ->
382 Blocks.bind_step_block
385 AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
386 List.list -> (Registers.register, Joint.joint_seq List.list)
389 val translate_store :
390 AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
391 List.list -> (Registers.register, Joint.joint_seq List.list)
394 val ensure_bind_step_block :
395 Joint.params -> AST.ident List.list -> (Registers.register, Joint.joint_seq
396 List.list) Bind_new.bind_new -> Blocks.bind_step_block
398 val translate_statement :
399 AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
400 -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
401 Blocks.bind_fin_block) Types.sum, __) Types.dPair
403 val translate_internal :
404 AST.ident List.list -> RTLabs_syntax.internal_function ->
405 Joint.joint_closed_internal_function
408 CostLabel.costlabel -> RTLabs_syntax.rTLabs_program -> RTL.rtl_program