99 open Hints_declaration
122 | PSD of Registers.register
123 | HDW of I8051.register
125 val move_dst_rect_Type4 :
126 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
128 val move_dst_rect_Type5 :
129 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
131 val move_dst_rect_Type3 :
132 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
134 val move_dst_rect_Type2 :
135 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
137 val move_dst_rect_Type1 :
138 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
140 val move_dst_rect_Type0 :
141 (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
143 val move_dst_inv_rect_Type4 :
144 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
147 val move_dst_inv_rect_Type3 :
148 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
151 val move_dst_inv_rect_Type2 :
152 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
155 val move_dst_inv_rect_Type1 :
156 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
159 val move_dst_inv_rect_Type0 :
160 move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
163 val move_dst_discr : move_dst -> move_dst -> __
165 val move_dst_jmdiscr : move_dst -> move_dst -> __
167 type move_src = move_dst Joint.argument
169 val move_src_from_dst : move_dst -> move_src
171 val dpi1__o__move_dst_to_src__o__inject :
172 (move_dst, 'a1) Types.dPair -> move_src Types.sig0
174 val eject__o__move_dst_to_src__o__inject :
175 move_dst Types.sig0 -> move_src Types.sig0
177 val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0
179 val dpi1__o__move_dst_to_src : (move_dst, 'a1) Types.dPair -> move_src
181 val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src
183 val psd_argument_move_src : Joint.psd_argument -> move_src
185 val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
186 BitVector.byte -> move_src Types.sig0
188 val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
189 (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
191 val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
192 (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
194 val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
195 (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
197 val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
198 BitVector.byte Types.sig0 -> move_src Types.sig0
200 val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
201 BitVector.byte Types.sig0 -> move_src Types.sig0
203 val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
204 Registers.register Types.sig0 -> move_src Types.sig0
206 val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
207 Registers.register -> move_src Types.sig0
209 val dpi1__o__psd_argument_to_move_src__o__inject :
210 (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0
212 val eject__o__psd_argument_to_move_src__o__inject :
213 Joint.psd_argument Types.sig0 -> move_src Types.sig0
215 val psd_argument_to_move_src__o__inject :
216 Joint.psd_argument -> move_src Types.sig0
218 val byte_to_psd_argument__o__psd_argument_to_move_src :
219 BitVector.byte -> move_src
221 val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
222 (BitVector.byte, 'a1) Types.dPair -> move_src
224 val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
225 (BitVector.byte, 'a1) Types.dPair -> move_src
227 val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
228 (Registers.register, 'a1) Types.dPair -> move_src
230 val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
231 BitVector.byte Types.sig0 -> move_src
233 val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
234 BitVector.byte Types.sig0 -> move_src
236 val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
237 Registers.register Types.sig0 -> move_src
239 val reg_to_psd_argument__o__psd_argument_to_move_src :
240 Registers.register -> move_src
242 val dpi1__o__psd_argument_to_move_src :
243 (Joint.psd_argument, 'a1) Types.dPair -> move_src
245 val eject__o__psd_argument_to_move_src :
246 Joint.psd_argument Types.sig0 -> move_src
251 | Ertl_frame_size of Registers.register
253 val ertl_seq_rect_Type4 :
254 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
256 val ertl_seq_rect_Type5 :
257 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
259 val ertl_seq_rect_Type3 :
260 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
262 val ertl_seq_rect_Type2 :
263 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
265 val ertl_seq_rect_Type1 :
266 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
268 val ertl_seq_rect_Type0 :
269 'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
271 val ertl_seq_inv_rect_Type4 :
272 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
275 val ertl_seq_inv_rect_Type3 :
276 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
279 val ertl_seq_inv_rect_Type2 :
280 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
283 val ertl_seq_inv_rect_Type1 :
284 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
287 val ertl_seq_inv_rect_Type0 :
288 ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
291 val ertl_seq_discr : ertl_seq -> ertl_seq -> __
293 val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __
295 val eRTL_uns : Joint.unserialized_params
297 val regs_from_move_dst : move_dst -> Registers.register List.list
299 val regs_from_move_src : move_src -> Registers.register List.list
301 val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list
303 val eRTL_functs : Joint.get_pseudo_reg_functs
305 val eRTL : Joint.graph_params
307 type ertl_program = Joint.joint_program
309 val dpi1__o__reg_to_ertl_snd_argument__o__inject :
310 (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
312 val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
313 (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
315 val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
316 (Registers.register, 'a1) Types.dPair -> move_src
318 val eject__o__reg_to_ertl_snd_argument__o__inject :
319 Registers.register Types.sig0 -> Joint.psd_argument Types.sig0
321 val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
322 Registers.register Types.sig0 -> move_src Types.sig0
324 val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
325 Registers.register Types.sig0 -> move_src
327 val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
328 Registers.register -> move_src
330 val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
331 Registers.register -> move_src Types.sig0
333 val reg_to_ertl_snd_argument__o__inject :
334 Registers.register -> Joint.psd_argument Types.sig0
336 val dpi1__o__reg_to_ertl_snd_argument :
337 (Registers.register, 'a1) Types.dPair -> Joint.psd_argument
339 val eject__o__reg_to_ertl_snd_argument :
340 Registers.register Types.sig0 -> Joint.psd_argument
342 val dpi1__o__byte_to_ertl_snd_argument__o__inject :
343 (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
345 val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
346 (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
348 val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
349 (BitVector.byte, 'a1) Types.dPair -> move_src
351 val eject__o__byte_to_ertl_snd_argument__o__inject :
352 BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0
354 val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
355 BitVector.byte Types.sig0 -> move_src Types.sig0
357 val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
358 BitVector.byte Types.sig0 -> move_src
360 val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
361 BitVector.byte -> move_src
363 val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
364 BitVector.byte -> move_src Types.sig0
366 val byte_to_ertl_snd_argument__o__inject :
367 BitVector.byte -> Joint.psd_argument Types.sig0
369 val dpi1__o__byte_to_ertl_snd_argument :
370 (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument
372 val eject__o__byte_to_ertl_snd_argument :
373 BitVector.byte Types.sig0 -> Joint.psd_argument
375 val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
377 val dpi1__o__ertl_seq_to_joint_seq__o__inject :
378 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0
380 val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
381 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0
383 val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
384 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
386 val eject__o__ertl_seq_to_joint_seq__o__inject :
387 AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0
389 val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
390 AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0
392 val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
393 AST.ident List.list -> __ Types.sig0 -> Joint.joint_step
395 val ertl_seq_to_joint_seq__o__seq_to_step :
396 AST.ident List.list -> __ -> Joint.joint_step
398 val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
399 AST.ident List.list -> __ -> Joint.joint_step Types.sig0
401 val ertl_seq_to_joint_seq__o__inject :
402 AST.ident List.list -> __ -> Joint.joint_seq Types.sig0
404 val dpi1__o__ertl_seq_to_joint_seq :
405 AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
407 val eject__o__ertl_seq_to_joint_seq :
408 AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq
410 val eRTL_premain : ertl_program -> Joint.joint_closed_internal_function